val lemma_div_pow2_le (a: int) (n m: nat)
    : Lemma (requires (m <= n /\ a <= pow2 n))
      (ensures (m <= n /\ a <= pow2 n /\ a / pow2 m <= pow2 (n - m)))
let lemma_div_pow2_le (a: int) (n m: nat) : Lemma
  (requires (m <= n /\ a <= pow2 n))
  (ensures (m <= n /\ a <= pow2 n /\ a / pow2 m <= pow2 (n - m)))
= if a = pow2 n
  then pow2_multiplication_division_lemma_1 1 m n
  else lemma_div_lt a n m
val lemma_div_pow2_le (a: int) (n m: nat)
    : Lemma (requires (m <= n /\ a <= pow2 n))
      (ensures (m <= n /\ a <= pow2 n /\ a / pow2 m <= pow2 (n - m)))
let lemma_div_pow2_le (a: int) (n m: nat)
    : Lemma (requires (m <= n /\ a <= pow2 n))
      (ensures (m <= n /\ a <= pow2 n /\ a / pow2 m <= pow2 (n - m))) =
if a = pow2 n then pow2_multiplication_division_lemma_1 1 m n else lemma_div_lt a n m
LowParse.Math.fst.checked
prims.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Math.Lemmas.fst.checked FStar.Classical.fsti.checked
LowParse.Math.fst
Prims.int Prims.nat Prims.op_Equality Prims.pow2 FStar.Math.Lemmas.pow2_multiplication_division_lemma_1 Prims.bool FStar.Math.Lemmas.lemma_div_lt Prims.unit Prims.l_and Prims.b2t Prims.op_LessThanOrEqual Prims.squash Prims.op_Division Prims.op_Subtraction Prims.Nil FStar.Pervasives.pattern
module LowParse.Math
include FStar.Math.Lemmas
open FStar.Mul

let mul_reg_r
  (a b x: int)
: Lemma
  (requires (
    x <> 0 /\
    a * x == b * x
  ))
  (ensures (a == b))
= ()

let mul_reg_l
  (x a b: int)
: Lemma
  (requires (
    x <> 0 /\
    x * a == x * b
  ))
  (ensures (a == b))
= ()

let lt_mul_add_reg_r
  (x y: nat)
  (s: pos)
: Lemma
  (requires (x * s < y * s + s))
  (ensures (x <= y))
= distributivity_add_left x (y + 1) s

let mult_decomp
  (i: pos) (j: nat)
: Lemma
  (i * j == j + (i - 1) * j)
= ()

let lemma_div_pow2_le (a: int) (n m: nat) : Lemma
  (requires (m <= n /\ a <= pow2 n))
val lemma_div_pow2_le (a: int) (n m: nat)
    : Lemma (requires (m <= n /\ a <= pow2 n))
      (ensures (m <= n /\ a <= pow2 n /\ a / pow2 m <= pow2 (n - m)))
a: Prims.int -> n: Prims.nat -> m: Prims.nat
  -> FStar.Pervasives.Lemma (requires m <= n /\ a <= Prims.pow2 n)
      (ensures m <= n /\ a <= Prims.pow2 n /\ a / Prims.pow2 m <= Prims.pow2 (n - m))