Example of matching loop

Here's an example of a matching loop found in the wild, that we could try to improve.

```fstar
module Min

open FStar.Tactics.Typeclasses
open FStar.Real
module SZ = FStar.SizeT

class can_approximate (c m : Type) = {
( %~ ) : c -> m -> prop;
}

inline_for_extraction noextract
class scalar (t : Type) = {
add : t -> t -> t;
zero : t;
v_approximates : t -> real -> prop;
a0 : squash (v_approximates zero 0.0R);
a_add : x:t -> y:t -> r:real -> s:real ->
Lemma (requires v_approximates x r /\ v_approximates y s)
(ensures v_approximates (x `add` y) (r +. s))
[SMTPat (v_approximates x r); SMTPat (v_approximates y s)]
;
}

let approx (#dom1 #dom2 #cod1 #cod2 : Type)
{| can_approximate dom1 dom2, can_approximate cod1 cod2 |}
(f1 : dom1 -> cod1) (f2 : dom2 -> cod2)
: prop
= forall x1 x2. x1 %~ x2 ==> f1 x1 %~ f2 x2

instance scalar_can_approx_reals (t:Type) (_ : scalar t) : can_approximate t real = {
(%~) = v_approximates;
}

let kpre
(et : Type) {| scalar et |}
(pre_map : et -> et)
(pre_map_r : real -> real)
(_ : pre_map `approx` pre_map_r)
(nth : nat { 0 < nth })
: nat
= 1 / nth
```
This fails very robustly (`--retry 100`) with `Subtyping check failed; Expected type nat got type int` i.e. it can't prove that `1 / nth >= 0`, though this is obvious since `nth > 0`. Z3 reports `(:reason-unknown "canceled")` i.e. hit the rlimit. Looking at the stats it reports, quantifier instantiation is somewhat high:
```
:quant-instantiations 2319
:rlimit-count 2548414
```
and it seems to grow as the rlimit increases, very quickly at first, then roughly linearly:
```
rlimit (F* units) -> quantifier instantiations
5 2319
10 16801
20 73075
40 185831
80 412723
160 879670
```

The matching loop is introduced by the combination of
- The fact that `zero %~ 0.0R`
- The congruence for addition `a_add`
- The approximation precondition in `kpre`

Removing any of these makes the issue go away. For example removing the precondition makes the proof instant:
```
:quant-instantiations 86
:rlimit-count 18546
:time 0.00)
```

Start with the F* reproducer in issue #4264 and rerun it with --retry 100 while recording the Z3 quantifier-instantiation and rlimit statistics. Compare behavior after removing each of the three identified ingredients: zero %~ 0.0R, the a_add congruence, and the kpre approximation precondition. Done means the matching loop is addressed without losing the intended proof.

Written by the indexing model from the issue text.