val iter_fun (#t: Type) (f: (t -> GTot t)) (n: nat) (x: t) : GTot t (decreases n)
let rec iter_fun
  (#t: Type)
  (f: (t -> GTot t))
  (n: nat)
  (x: t)
: GTot t
  (decreases n)
= if n = 0
  then x
  else iter_fun f (n - 1) (f x)
val iter_fun (#t: Type) (f: (t -> GTot t)) (n: nat) (x: t) : GTot t (decreases n)
let rec iter_fun (#t: Type) (f: (t -> GTot t)) (n: nat) (x: t) : GTot t (decreases n) =
if n = 0 then x else iter_fun f (n - 1) (f x)
Steel.ST.GenArraySwap.Proof.fst.checked
prims.fst.checked FStar.Tactics.Effect.fsti.checked FStar.Tactics.CanonCommSemiring.fst.checked FStar.Tactics.fst.checked FStar.SizeT.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Math.Lemmas.fst.checked FStar.Classical.fsti.checked
Steel.ST.GenArraySwap.Proof.fst
Prims.nat Prims.op_Equality Prims.int Prims.bool Steel.ST.GenArraySwap.Proof.iter_fun Prims.op_Subtraction
module Steel.ST.GenArraySwap.Proof
open FStar.Math.Lemmas
open FStar.Mul

let lemma_mod_lt
  (a:int)
  (b:pos)
: Lemma
  (let r = a % b in 0 <= r /\ r < b)
  [SMTPat (a % b)]
= ()

let lemma_mul_nat_nat_is_nat
  (a b: nat)
: Lemma
  (a * b >= 0)
  [SMTPat (a * b)]
= ()

let lemma_pos_mul_pos_args
  (a: nat)
  (b: nat)
: Lemma
  (requires (a * b > 0))
  (ensures (a > 0 /\ b > 0 /\ a <= a * b /\ b <= a * b /\ a * b == b * a))
= ()

let lemma_div_nat
  (a: nat)
  (b: pos)
: Lemma
  (a / b >= 0)
  [SMTPat (a / b)]
= ()

let lemma_mult_reg_l
  (k: int)
  (x1 x2: int)
: Lemma
  (requires (
    k * x1 == k * x2 /\
    k <> 0
  ))
  (ensures (
    x1 == x2
  ))
= ()

let lemma_bezout_one_zero
  (x1: int)
  (x2: nat)
  (y1 y2: int)
: Lemma
  (requires (
    x1 * x2 + y1 * y2 == 1 /\
    y1 == 0
  ))
  (ensures (
    x1 == 1 /\ x2 == 1
  ))
= ()

#set-options "--z3cliopt smt.arith.nl=false"

let int_semiring () =
  FStar.Tactics.CanonCommSemiring.int_semiring ();
  FStar.Tactics.trefl ();
  FStar.Tactics.qed ()

[@@erasable]
noeq
type bezout_t = {
  d: pos;
  q_n: nat;
  q_l: nat;
  u_n: int;
  u_l: int;
}

let bezout_prop'
  (n: nat)
  (l: nat)
  (d: pos)
  (q_n: nat)
  (q_l: nat)
  (u_n: int)
  (u_l: int)
: Tot prop
= n == d * q_n /\
  l == d * q_l /\
  d == n * u_n + l * u_l

let bezout_prop
  (n: nat)
  (l: nat)
  (b: bezout_t)
: Tot prop
= bezout_prop' n l b.d b.q_n b.q_l b.u_n b.u_l

let bezout
  (n: nat)
  (l: nat)
: Tot Type
= (b: bezout_t { bezout_prop n l b })

#restart-solver
let rec mk_bezout
  (n: pos)
  (l: nat)
: Pure (bezout n l)
  (requires (l < n))
  (ensures (fun _ -> True))
  (decreases l)
= if l = 0
  then begin
    let d : pos = n in
    let q_n : nat = 1 in
    let q_l : nat = 0 in
    let u_n : int = 1 in
    let u_l : int = 0 in
    let res = {
      d = d;
      q_n = q_n;
      q_l = q_l;
      u_n = u_n;
      u_l = u_l;
    }
    in
    assert (eq2 #int n (d * q_n)) by (int_semiring ());
    assert (eq2 #int 0 (d * q_l)) by (int_semiring ());
    assert (eq2 #int d (n * 1 + 0 * res.u_l)) by (int_semiring ());
    res
  end
  else begin
    let lpre = n % l in
    let ql = n / l in
    euclidean_division_definition n l;
    let bpre = mk_bezout l lpre in
    let d = bpre.d in
    let q_l = bpre.q_n in
    let qpre_lpre = bpre.q_l in
    let upre_l = bpre.u_n in
    let upre_lpre = bpre.u_l in
    let n_alt0 = l * ql + lpre in
    assert (n == n_alt0);
    let l_alt = d * q_l in
    let lpre_alt1 = d * qpre_lpre in
    let n_alt1 = l_alt * ql + lpre_alt1 in
    assert (n_alt1 == n);
    let q_n = q_l * ql + qpre_lpre in
    assert (eq2 #int n_alt1 (d * q_n)) by (int_semiring ());
    let lpre_alt2 = n + - l * ql in
    assert (lpre_alt2 == lpre);
    let d_alt = l * upre_l + lpre_alt2 * upre_lpre in
    assert (d_alt == d);
    let u_l = upre_l + - ql * upre_lpre in
    assert (eq2 #int (n * upre_lpre + l * u_l) d_alt) by (int_semiring ());
    let res = {
      d = d;
      q_n = q_n;
      q_l = q_l;
      u_n = upre_lpre;
      u_l = u_l;
    }
    in
    res
  end

let bezout_q_eq
  (n: nat)
  (l: nat)
  (bz: bezout n l)
: Lemma
  (bz.q_n == n / bz.d)
  [SMTPat (bezout_prop n l bz); SMTPat bz.q_n]
= cancel_mul_div bz.q_n bz.d

let rec iter_fun
  (#t: Type)
  (f: (t -> GTot t))
  (n: nat)
  (x: t)
: GTot t
val iter_fun (#t: Type) (f: (t -> GTot t)) (n: nat) (x: t) : GTot t (decreases n)
f: (_: t -> Prims.GTot t) -> n: Prims.nat -> x: t -> Prims.GTot t