val lt_mul_add_reg_r (x y: nat) (s: pos) : Lemma (requires (x * s < y * s + s)) (ensures (x <= y))
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
val lt_mul_add_reg_r (x y: nat) (s: pos) : Lemma (requires (x * s < y * s + s)) (ensures (x <= y))
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
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.nat Prims.pos FStar.Math.Lemmas.distributivity_add_left Prims.op_Addition Prims.unit Prims.b2t Prims.op_LessThan FStar.Mul.op_Star Prims.squash Prims.op_LessThanOrEqual 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))
val lt_mul_add_reg_r (x y: nat) (s: pos) : Lemma (requires (x * s < y * s + s)) (ensures (x <= y))
x: Prims.nat -> y: Prims.nat -> s: Prims.pos
  -> FStar.Pervasives.Lemma (requires x * s < y * s + s) (ensures x <= y)