val nat_to_two_to_nat (n1 n2:nat32) : Lemma
  (nat_to_two 32 (two_to_nat 32 (Mktwo n1 n2)) == Mktwo n1 n2)
  [SMTPat (nat_to_two 32 (two_to_nat 32 (Mktwo n1 n2)))]
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;
  ()
val nat_to_two_to_nat (n1 n2:nat32) : Lemma
  (nat_to_two 32 (two_to_nat 32 (Mktwo n1 n2)) == Mktwo n1 n2)
  [SMTPat (nat_to_two 32 (two_to_nat 32 (Mktwo n1 n2)))]
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 (nat_to_two 32 n == Mktwo (n % pow2_32) ((n / pow2_32) % pow2_32));
lemma_fundamental_div_mod n;
()
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
Vale.Def.Words_s.nat32 Prims.unit Vale.Def.Words.Two.lemma_fundamental_div_mod FStar.Pervasives.assert_norm Prims.eq2 Vale.Def.Words_s.two Vale.Def.Words_s.natN Prims.pow2 Vale.Def.Words.Two_s.nat_to_two Vale.Def.Words_s.Mktwo Prims.op_Modulus Vale.Def.Words_s.pow2_32 Prims.op_Division Prims.int Vale.Def.Words_s.pow2_norm Prims._assert Vale.Def.Words.Two_s.two_to_nat Prims.b2t Prims.op_LessThan Vale.Def.Words_s.pow2_64 Prims.op_LessThanOrEqual Vale.Def.Words_s.int_to_natN Prims.op_Addition FStar.Mul.op_Star Prims.l_True Prims.squash Prims.Nil FStar.Pervasives.pattern
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
val nat_to_two_to_nat (n1 n2:nat32) : Lemma
  (nat_to_two 32 (two_to_nat 32 (Mktwo n1 n2)) == Mktwo n1 n2)
  [SMTPat (nat_to_two 32 (two_to_nat 32 (Mktwo n1 n2)))]
n1: Vale.Def.Words_s.nat32 -> n2: Vale.Def.Words_s.nat32
  -> FStar.Pervasives.Lemma
      (ensures
        Vale.Def.Words.Two_s.nat_to_two 32
          (Vale.Def.Words.Two_s.two_to_nat 32 (Vale.Def.Words_s.Mktwo n1 n2)) ==
        Vale.Def.Words_s.Mktwo n1 n2)
      [
        SMTPat (Vale.Def.Words.Two_s.nat_to_two 32
              (Vale.Def.Words.Two_s.two_to_nat 32 (Vale.Def.Words_s.Mktwo n1 n2)))
      ]