From eb8dbc102095c3e5fc3c733c540a4a4181375cea Mon Sep 17 00:00:00 2001
From: Adrien Champion <adrien.champion@protonmail.com>
Date: Mon, 22 Jul 2024 16:40:09 +0200
Subject: [PATCH] feat: more useful Int/Rat lemmas

---
 Smt/Reconstruct/Int/Core.lean |  7 +++++++
 Smt/Reconstruct/Rat/Core.lean | 20 ++++++++++++++++++++
 2 files changed, 27 insertions(+)

diff --git a/Smt/Reconstruct/Int/Core.lean b/Smt/Reconstruct/Int/Core.lean
index 27f1549b..e0b3395e 100644
--- a/Smt/Reconstruct/Int/Core.lean
+++ b/Smt/Reconstruct/Int/Core.lean
@@ -49,6 +49,13 @@ protected theorem dvd_mul_left_of_dvd {i j : Int} (k : Int) : i ∣ j → i ∣
     Int.mul_assoc i k n,
   ]
 
+protected theorem natAbs_gcd_dvd {i : Int} {n : Nat} : ↑(i.natAbs.gcd n) ∣ i := by
+  refine ofNat_dvd_left.mpr ?_
+  exact Nat.gcd_dvd_left _ _
+
+protected theorem natAbs_gcd_dvd' (i : Int) (n : Nat) : ↑(i.natAbs.gcd n) ∣ i :=
+  Int.natAbs_gcd_dvd
+
 protected theorem dvd_mul_right_of_dvd {i j : Int} (k : Int) : i ∣ j → i ∣ j * k :=
   Int.mul_comm j k ▸ Int.dvd_mul_left_of_dvd k
 
diff --git a/Smt/Reconstruct/Rat/Core.lean b/Smt/Reconstruct/Rat/Core.lean
index bce94b2a..7a99eb1e 100644
--- a/Smt/Reconstruct/Rat/Core.lean
+++ b/Smt/Reconstruct/Rat/Core.lean
@@ -23,6 +23,26 @@ theorem num_divInt_den (q : Rat) : q.num /. q.den = q :=
 theorem mk'_eq_divInt {n d h c} : (⟨n, d, h, c⟩ : Rat) = n /. d :=
   (num_divInt_den _).symm
 
+theorem divInt_num (q : Rat) : (q.num /. q.den).num = q.num := by
+  simp [mkRat, q.den_nz, normalize, Rat.reduced]
+
+theorem divInt_num'
+  {n : Int} {d : Nat}
+  (nz_d : d ≠ 0 := by omega)
+  (reduced : n.natAbs.Coprime d := by assumption)
+: (n /. d).num = n := by
+  simp [mkRat, nz_d, normalize, reduced]
+
+theorem divInt_den (q : Rat) : (q.num /. q.den).den = q.den := by
+  simp [mkRat, q.den_nz, normalize, Rat.reduced]
+
+theorem divInt_den'
+  {n : Int} {d : Nat}
+  (nz_d : d ≠ 0 := by omega)
+  (reduced : n.natAbs.Coprime d := by assumption)
+: (n /. d).den = d := by
+  simp [mkRat, nz_d, normalize, reduced]
+
 @[elab_as_elim]
 def numDenCasesOn.{u} {C : Rat → Sort u}
 : ∀ (a : Rat) (_ : ∀ n d, 0 < d → (Int.natAbs n).Coprime d → C (n /. d)), C a