val two_to_nat_32_injective (_:unit) : Lemma
  (forall (x x':two (natN (pow2_norm 32))).{:pattern two_to_nat 32 x; two_to_nat 32 x'}
    two_to_nat 32 x == two_to_nat 32 x' ==> x == x')
let two_to_nat_32_injective () =
  generic_injective_proof (two_to_nat 32) (nat_to_two 32) (fun x -> nat_to_two_to_nat x.lo x.hi)
val two_to_nat_32_injective (_:unit) : Lemma
  (forall (x x':two (natN (pow2_norm 32))).{:pattern two_to_nat 32 x; two_to_nat 32 x'}
    two_to_nat 32 x == two_to_nat 32 x' ==> x == x')
let two_to_nat_32_injective () =
generic_injective_proof (two_to_nat 32) (nat_to_two 32) (fun x -> nat_to_two_to_nat x.lo x.hi)
Vale.Def.Words.Two.fst.checked
Vale.Lib.Meta.fsti.checked prims.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked
Vale.Def.Words.Two.fst
Prims.unit Vale.Lib.Meta.generic_injective_proof Vale.Def.Words_s.two Vale.Def.Words_s.nat32 Vale.Def.Words_s.natN Prims.pow2 FStar.Mul.op_Star Vale.Def.Words.Two_s.two_to_nat Vale.Def.Words.Two_s.nat_to_two Vale.Def.Words.Two.nat_to_two_to_nat Vale.Def.Words_s.__proj__Mktwo__item__lo Vale.Def.Words_s.__proj__Mktwo__item__hi
module Vale.Def.Words.Two
open FStar.Mul
open Vale.Lib.Meta

let lemma_fundamental_div_mod (x:nat64) :
  Lemma (x = x % pow2_32 + pow2_32 * ((x / pow2_32) % pow2_32))
  =
  ()

let nat_to_two_to_nat (n1 n2:nat32) : Lemma
  (nat_to_two 32 (two_to_nat 32 (Mktwo n1 n2)) == Mktwo n1 n2)
  =
  let n = n1 + n2 * pow2_32 in
  assert_norm (two_to_nat 32 (Mktwo n1 n2) == int_to_natN pow2_64 n);
  assert (0 <= n);
  assert (n < pow2_64);
  assert (two_to_nat 32 (Mktwo n1 n2) == n);
  assert_norm (pow2_norm 32 == pow2_32);
  //assert_norm (pow2_norm (2 * 32) == pow2_64);
  assert_norm (nat_to_two 32 n == Mktwo (n % pow2_32) ((n / pow2_32) % pow2_32));
  lemma_fundamental_div_mod n;
  ()

let two_to_nat_to_two (n:nat64) =
  let n1 = n % (pow2_32) in
  let n2 = (n/(pow2_32)) % (pow2_32) in
  let n_f = two_to_nat 32 (Mktwo n1 n2) in
  assert_norm (n == n1 + n2 * pow2_32)
val two_to_nat_32_injective (_:unit) : Lemma
  (forall (x x':two (natN (pow2_norm 32))).{:pattern two_to_nat 32 x; two_to_nat 32 x'}
    two_to_nat 32 x == two_to_nat 32 x' ==> x == x')
_: Prims.unit
  -> FStar.Pervasives.Lemma
    (ensures
      forall (x: Vale.Def.Words_s.two (Vale.Def.Words_s.natN (Vale.Def.Words_s.pow2_norm 32)))
        (x': Vale.Def.Words_s.two (Vale.Def.Words_s.natN (Vale.Def.Words_s.pow2_norm 32))).
        {:pattern Vale.Def.Words.Two_s.two_to_nat 32 x; Vale.Def.Words.Two_s.two_to_nat 32 x'}
        Vale.Def.Words.Two_s.two_to_nat 32 x == Vale.Def.Words.Two_s.two_to_nat 32 x' ==> x == x')