val bezout_prop (n l: nat) (b: bezout_t) : Tot prop
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
val bezout_prop (n l: nat) (b: bezout_t) : Tot prop
let bezout_prop (n 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
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 Steel.ST.GenArraySwap.Proof.bezout_t Steel.ST.GenArraySwap.Proof.bezout_prop' Steel.ST.GenArraySwap.Proof.__proj__Mkbezout_t__item__d Steel.ST.GenArraySwap.Proof.__proj__Mkbezout_t__item__q_n Steel.ST.GenArraySwap.Proof.__proj__Mkbezout_t__item__q_l Steel.ST.GenArraySwap.Proof.__proj__Mkbezout_t__item__u_n Steel.ST.GenArraySwap.Proof.__proj__Mkbezout_t__item__u_l Prims.prop
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)
val bezout_prop (n l: nat) (b: bezout_t) : Tot prop
n: Prims.nat -> l: Prims.nat -> b: Steel.ST.GenArraySwap.Proof.bezout_t -> Prims.prop