val gcd_inv_prop (n0 l0 n l: nat) (b: bool) : Tot prop
let gcd_inv_prop
  (n0: nat)
  (l0: nat)
  (n: nat)
  (l: nat)
  (b: bool)
: Tot prop
= l0 < n0 /\
  l < n /\
  (Prf.mk_bezout n0 l0).d == (Prf.mk_bezout n l).d /\
  b == (l > 0)
val gcd_inv_prop (n0 l0 n l: nat) (b: bool) : Tot prop
let gcd_inv_prop (n0 l0 n l: nat) (b: bool) : Tot prop =
l0 < n0 /\ l < n /\ (Prf.mk_bezout n0 l0).d == (Prf.mk_bezout n l).d /\ b == (l > 0)
Steel.ST.GenArraySwap.fst.checked
Steel.ST.Reference.fsti.checked Steel.ST.Loops.fsti.checked Steel.ST.GenElim.fsti.checked Steel.ST.GenArraySwap.Proof.fst.checked prims.fst.checked FStar.SizeT.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Ghost.fsti.checked
Steel.ST.GenArraySwap.fst
Prims.nat Prims.bool Prims.l_and Prims.b2t Prims.op_LessThan Prims.eq2 Prims.pos Steel.ST.GenArraySwap.Proof.__proj__Mkbezout_t__item__d Steel.ST.GenArraySwap.Proof.mk_bezout Prims.op_GreaterThan Prims.prop
module Steel.ST.GenArraySwap
open Steel.ST.GenElim

module Prf = Steel.ST.GenArraySwap.Proof
module R = Steel.ST.Reference

let gcd_inv_prop
  (n0: nat)
  (l0: nat)
  (n: nat)
  (l: nat)
  (b: bool)
val gcd_inv_prop (n0 l0 n l: nat) (b: bool) : Tot prop
n0: Prims.nat -> l0: Prims.nat -> n: Prims.nat -> l: Prims.nat -> b: Prims.bool -> Prims.prop