val lemma_quad32_ones (_:unit) : Lemma
  (let q = Mkfour 0xffffffff 0xffffffff 0xffffffff 0xffffffff in of_quad32 q == ones 128 /\ q == to_quad32 (ones 128))
let lemma_quad32_ones () =
  let n = 0xffffffff in
  lemma_bitwise_all ();
  lemma_equal (ones 128) (poly128_of_nat32s n n n n);
  lemma_quad32_of_nat32s n n n n;
  lemma_of_to_quad32 (ones 128);
  ()
val lemma_quad32_ones (_:unit) : Lemma
  (let q = Mkfour 0xffffffff 0xffffffff 0xffffffff 0xffffffff in of_quad32 q == ones 128 /\ q == to_quad32 (ones 128))
let lemma_quad32_ones () =
let n = 0xffffffff in
lemma_bitwise_all ();
lemma_equal (ones 128) (poly128_of_nat32s n n n n);
lemma_quad32_of_nat32s n n n n;
lemma_of_to_quad32 (ones 128);
()
Vale.Math.Poly2.Words.fst.checked
prims.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Calc.fsti.checked
Vale.Math.Poly2.Words.fst
Prims.unit Vale.Math.Poly2.Bits.lemma_of_to_quad32 Vale.Math.Poly2.ones Vale.Math.Poly2.Bits.lemma_quad32_of_nat32s Vale.Math.Poly2.lemma_equal Vale.Math.Poly2.Bits.poly128_of_nat32s Vale.Math.Poly2.Lemmas.lemma_bitwise_all Prims.int
module Vale.Math.Poly2.Words
open FStar.Mul

let lemma_quad32_zero () =
  lemma_bitwise_all ();
  lemma_equal zero (poly128_of_nat32s 0 0 0 0);
  lemma_quad32_of_nat32s 0 0 0 0;
  lemma_of_to_quad32 zero;
  ()
val lemma_quad32_ones (_:unit) : Lemma
  (let q = Mkfour 0xffffffff 0xffffffff 0xffffffff 0xffffffff in of_quad32 q == ones 128 /\ q == to_quad32 (ones 128))
_: Prims.unit
  -> FStar.Pervasives.Lemma
    (ensures
      (let q = Vale.Def.Words_s.Mkfour 0xffffffff 0xffffffff 0xffffffff 0xffffffff in
        Vale.Math.Poly2.Bits_s.of_quad32 q == Vale.Math.Poly2.ones 128 /\
        q == Vale.Math.Poly2.Bits_s.to_quad32 (Vale.Math.Poly2.ones 128)))