val lemma_as_nat5: f:qelem5 ->
  Lemma
  (requires qelem_fits5 f (1, 1, 1, 1, 1))
  (ensures  as_nat5 f < pow2 280)
let lemma_as_nat5 f =
  //let (f0, f1, f2, f3, f4) = f in
  //assert (as_nat5 f == v f0 + v f1 * pow56 + v f2 * pow112 + v f3 * pow168 + v f4 * pow224);
  assert_norm (pow2 56 * pow2 56 = pow2 112);
  assert_norm (pow2 56 * pow2 112 = pow2 168);
  assert_norm (pow2 56 * pow2 168 = pow2 224);
  assert_norm (pow2 56 * pow2 224 = pow2 280)
val lemma_as_nat5: f:qelem5 ->
  Lemma
  (requires qelem_fits5 f (1, 1, 1, 1, 1))
  (ensures  as_nat5 f < pow2 280)
let lemma_as_nat5 f =
assert_norm (pow2 56 * pow2 56 = pow2 112);
assert_norm (pow2 56 * pow2 112 = pow2 168);
assert_norm (pow2 56 * pow2 168 = pow2 224);
assert_norm (pow2 56 * pow2 224 = pow2 280)
Hacl.Spec.BignumQ.Lemmas.fst.checked
Spec.Ed25519.fst.checked prims.fst.checked Lib.IntTypes.fsti.checked Hacl.Spec.BignumQ.Definitions.fst.checked FStar.UInt32.fsti.checked FStar.Tactics.Effect.fsti.checked FStar.Tactics.CanonCommSemiring.fst.checked FStar.Tactics.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Math.Lemmas.fst.checked FStar.Calc.fsti.checked
Hacl.Spec.BignumQ.Lemmas.fst
Hacl.Spec.BignumQ.Definitions.qelem5 FStar.Pervasives.assert_norm Prims.b2t Prims.op_Equality Prims.int FStar.Mul.op_Star Prims.pow2 Prims.unit
module Hacl.Spec.BignumQ.Lemmas

open FStar.Tactics.CanonCommSemiring
open FStar.Mul
open Lib.IntTypes

module S = Spec.Ed25519

include Hacl.Spec.BignumQ.Definitions

let feq (#a #b:Type) (f:(a -> b)) (x y:a) :
  Lemma (requires x == y) (ensures f x == f y) = ()

let eq_eq2 (#a:eqtype) (x y:a) :
  Lemma (requires x = y) (ensures x == y) = ()

val lemma_mul_lt:a:nat -> b:nat -> c:nat -> d:nat ->
  Lemma
  (requires a < b /\ c < d)
  (ensures  a * c < b * d)

let lemma_mul_lt a b c d = ()


val lemma_as_nat5: f:qelem5 ->
  Lemma
  (requires qelem_fits5 f (1, 1, 1, 1, 1))
  (ensures  as_nat5 f < pow2 280)

let lemma_as_nat5 f =
  //let (f0, f1, f2, f3, f4) = f in
val lemma_as_nat5: f:qelem5 ->
  Lemma
  (requires qelem_fits5 f (1, 1, 1, 1, 1))
  (ensures  as_nat5 f < pow2 280)
f: Hacl.Spec.BignumQ.Definitions.qelem5
  -> FStar.Pervasives.Lemma (requires Hacl.Spec.BignumQ.Definitions.qelem_fits5 f (1, 1, 1, 1, 1))
      (ensures Hacl.Spec.BignumQ.Definitions.as_nat5 f < Prims.pow2 280)