val lemma_exact_mul: a:nat -> b:pos -> c:nat ->
    Lemma (requires (c % b = 0))
          (ensures ((a*c) % b = 0))
let lemma_exact_mul a b c =
  (* a*c = c*a *)
  swap_mul a c;

  (* (c*a)%b = ((c%b)*a)%b *)
  lemma_mod_mul_distr_l c a b;
  ()
val lemma_exact_mul: a:nat -> b:pos -> c:nat ->
    Lemma (requires (c % b = 0))
          (ensures ((a*c) % b = 0))
let lemma_exact_mul a b c =
swap_mul a c;
lemma_mod_mul_distr_l c a b;
()
Vale.Poly1305.Math.fst.checked
Vale.Poly1305.Bitvectors.fsti.checked Vale.Math.Lemmas.Int.fsti.checked Vale.Def.TypesNative_s.fst.checked Vale.Arch.TypesNative.fsti.checked prims.fst.checked FStar.UInt.fsti.checked FStar.Tactics.Effect.fsti.checked FStar.Tactics.CanonCommSemiring.fst.checked FStar.Tactics.Canon.fst.checked FStar.Tactics.BV.fst.checked FStar.Tactics.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Math.Lemmas.fst.checked FStar.Classical.fsti.checked
Vale.Poly1305.Math.fst
Prims.nat Prims.pos Prims.unit Vale.Math.Lemmas.Int.lemma_mod_mul_distr_l FStar.Math.Lemmas.swap_mul
module Vale.Poly1305.Math

open FStar.Tactics
open FStar.Tactics.Canon
open FStar.Math.Lemmas
// open FStar.Math.Lib
open Vale.Math.Lemmas.Int
open FStar.Tactics.CanonCommSemiring
open FStar.Mul
open Vale.Def.TypesNative_s
open Vale.Arch.TypesNative
open FStar.Classical
open Vale.Poly1305.Bitvectors

#reset-options "--smtencoding.elim_box true --z3cliopt smt.arith.nl=true --max_fuel 1 --max_ifuel 1 --smtencoding.nl_arith_repr native --z3rlimit 100 --using_facts_from Prims --using_facts_from FStar.Math.Lemmas"

val lemma_mul_div_comm: a:nat -> b:pos -> c:nat ->
    Lemma (requires (c % b = 0 /\ a % b = 0))
          (ensures (a/b)*c == a * (c/b))
let lemma_mul_div_comm a b c =
    ()

val lemma_exact_mul: a:nat -> b:pos -> c:nat ->
    Lemma (requires (c % b = 0))
          (ensures ((a*c) % b = 0))
let lemma_exact_mul a b c =
val lemma_exact_mul: a:nat -> b:pos -> c:nat ->
    Lemma (requires (c % b = 0))
          (ensures ((a*c) % b = 0))
a: Prims.nat -> b: Prims.pos -> c: Prims.nat
  -> FStar.Pervasives.Lemma (requires c % b = 0) (ensures a * c % b = 0)