val divides_plus (a b d:int) : Lemma
  (requires d `divides` a /\ d `divides` b)
  (ensures  d `divides` (a + b))
let divides_plus a b d =
  Classical.exists_elim (d `divides` (a + b)) (Squash.get_proof (exists q1. a = q1 * d))
    (fun q1 ->
      Classical.exists_elim (d `divides` (a + b)) (Squash.get_proof (exists q2. b = q2 * d))
        (fun q2 ->
          assert (a + b = q1 * d + q2 * d);
          distributivity_add_left q1 q2 d;
          Classical.exists_intro (fun q -> a + b = q * d) (q1 + q2)))
val divides_plus (a b d:int) : Lemma
  (requires d `divides` a /\ d `divides` b)
  (ensures  d `divides` (a + b))
let divides_plus a b d =
Classical.exists_elim (d `divides` (a + b))
  (Squash.get_proof (exists q1. a = q1 * d))
  (fun q1 ->
      Classical.exists_elim (d `divides` (a + b))
        (Squash.get_proof (exists q2. b = q2 * d))
        (fun q2 ->
            assert (a + b = q1 * d + q2 * d);
            distributivity_add_left q1 q2 d;
            Classical.exists_intro (fun q -> a + b = q * d) (q1 + q2)))
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_elim FStar.Math.Euclid.divides Prims.op_Addition Prims.b2t Prims.op_Equality FStar.Mul.op_Star FStar.Squash.get_proof Prims.l_Exists FStar.Classical.exists_intro Prims.unit FStar.Math.Lemmas.distributivity_add_left Prims._assert Prims.squash
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
///

let divides_reflexive a =
  Classical.exists_intro (fun q -> a = q * a) 1

let divides_transitive a b c =
  eliminate exists q1. b == q1 * a
  returns a `divides` c
  with _pf. 
    eliminate exists q2. c == q2 * b
    returns _
    with _pf2.
         introduce exists q. c == q * a
	 with (q1 * q2)
	 and ()


let divide_antisym a b =
  if a <> 0 then
    Classical.exists_elim (a = b \/ a = -b) (Squash.get_proof (exists q1. b = q1 * a))
      (fun q1 ->
        Classical.exists_elim (a = b \/ a = -b) (Squash.get_proof (exists q2. a = q2 * b))
          (fun q2 ->
            assert (b = q1 * a);
            assert (a = q2 * b);
            assert (b = q1 * (q2 * b));
            paren_mul_right q1 q2 b;
            eq_mult_left b (q1 * q2);
            eq_mult_one q1 q2))

let divides_0 a =
  Classical.exists_intro (fun q -> 0 = q * a) 0

let divides_1 a = ()

let divides_minus a b =
  Classical.exists_elim (a `divides` (-b))
    (Squash.get_proof (a `divides` b))
    (fun q -> Classical.exists_intro (fun q' -> -b = q' * a) (-q))

let divides_opp a b =
  Classical.exists_elim ((-a) `divides` b)
    (Squash.get_proof (a `divides` b))
    (fun q -> Classical.exists_intro (fun q' -> b = q' * (-a)) (-q))
val divides_plus (a b d:int) : Lemma
  (requires d `divides` a /\ d `divides` b)
  (ensures  d `divides` (a + b))
a: Prims.int -> b: Prims.int -> d: Prims.int
  -> FStar.Pervasives.Lemma
      (requires FStar.Math.Euclid.divides d a /\ FStar.Math.Euclid.divides d b)
      (ensures FStar.Math.Euclid.divides d (a + b))