val lemma_quad32_zero (_:unit) : Lemma
  (of_quad32 (Mkfour 0 0 0 0) == zero /\ Mkfour 0 0 0 0 == to_quad32 zero)
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_zero (_:unit) : Lemma
  (of_quad32 (Mkfour 0 0 0 0) == zero /\ Mkfour 0 0 0 0 == to_quad32 zero)
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;
()
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_s.zero 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
module Vale.Math.Poly2.Words
open FStar.Mul
val lemma_quad32_zero (_:unit) : Lemma
  (of_quad32 (Mkfour 0 0 0 0) == zero /\ Mkfour 0 0 0 0 == to_quad32 zero)
_: Prims.unit
  -> FStar.Pervasives.Lemma
    (ensures
      Vale.Math.Poly2.Bits_s.of_quad32 (Vale.Def.Words_s.Mkfour 0 0 0 0) == Vale.Math.Poly2_s.zero /\
      Vale.Def.Words_s.Mkfour 0 0 0 0 == Vale.Math.Poly2.Bits_s.to_quad32 Vale.Math.Poly2_s.zero)