val divides_reflexive (a:int) : Lemma (a `divides` a) [SMTPat (a `divides` a)]
let divides_reflexive a =
  Classical.exists_intro (fun q -> a = q * a) 1
val divides_reflexive (a:int) : Lemma (a `divides` a) [SMTPat (a `divides` a)]
let divides_reflexive a =
Classical.exists_intro (fun q -> a = q * a) 1
FStar.Math.Euclid.fst.checked
prims.fst.checked FStar.Tactics.Effect.fsti.checked FStar.Tactics.Canon.fst.checked FStar.Squash.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Math.Lemmas.fst.checked FStar.Classical.Sugar.fsti.checked FStar.Classical.fsti.checked FStar.Calc.fsti.checked
FStar.Math.Euclid.fst
Prims.int FStar.Classical.exists_intro Prims.b2t Prims.op_Equality FStar.Mul.op_Star Prims.unit
module FStar.Math.Euclid

open FStar.Mul
open FStar.Math.Lemmas

///
/// Auxiliary lemmas
///

val eq_mult_left (a b:int) : Lemma (requires a = b * a) (ensures a = 0 \/ b = 1)
let eq_mult_left a b = ()

val eq_mult_one (a b:int) : Lemma
  (requires a * b = 1)
  (ensures (a = 1 /\ b = 1) \/ (a = -1 /\ b = -1))
let eq_mult_one a b = ()

val opp_idempotent (a:int) : Lemma (-(-a) == a)
let opp_idempotent a = ()

val add_sub_l (a b:int) : Lemma (a - b + b = a)
let add_sub_l a b = ()

val add_sub_r (a b:int) : Lemma (a + b - b = a)
let add_sub_r a b = ()

///
/// Divides relation
///
val divides_reflexive (a:int) : Lemma (a `divides` a) [SMTPat (a `divides` a)]
a: Prims.int
  -> FStar.Pervasives.Lemma (ensures FStar.Math.Euclid.divides a a)
      [SMTPat (FStar.Math.Euclid.divides a a)]