Built with doc-gen4, running Lean4. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+āCtrl+āto navigate, Ctrl+š±ļøto focus. On Mac, use Cmdinstead of Ctrl.
```/-
Authors: Jeremy Avigad, Leonardo de Moura, Mario Carneiro
-/
import Std.Data.Nat.Lemmas

/-!
# Definitions and properties of `gcd`, `lcm`, and `coprime`

-/

namespace Nat

theorem gcd_rec: ā (m n : Nat), gcd m n = gcd (n % m) mgcd_rec (m: Natm n: Natn : Nat: TypeNat) : gcd: Nat ā Nat ā Natgcd m: Natm n: Natn = gcd: Nat ā Nat ā Natgcd (n: Natn % m: Natm) m: Natm :=
match m: Natm with
| 0: Nat0 => byGoals accomplished! š m, n: Natgcd 0 n = gcd (n % 0) 0have := (mod_zero: ā (a : Nat), a % 0 = amod_zero n: Natn).symm: ā {Ī± : Sort ?u.189} {a b : Ī±}, a = b ā b = asymmm, n: Natthis: n = n % 0gcd 0 n = gcd (n % 0) 0;m, n: Natthis: n = n % 0gcd 0 n = gcd (n % 0) 0 m, n: Natgcd 0 n = gcd (n % 0) 0rwa [m, n: Natthis: n = n % 0gcd 0 n = gcd (n % 0) 0gcd_zero_right: ā (n : Nat), gcd n 0 = ngcd_zero_rightm, n: Natthis: n = n % 0gcd 0 n = n % 0]m, n: Natthis: n = n % 0gcd 0 n = n % 0
| _: Nat_ + 1 => byGoals accomplished! š m, n, nā: Natgcd (nā + 1) n = gcd (n % (nā + 1)) (nā + 1)simp [gcd_succ: ā (x y : Nat), gcd (succ x) y = gcd (y % succ x) (succ x)gcd_succ]Goals accomplished! š

@[elab_as_elim] theorem gcd.induction: ā {P : Nat ā Nat ā Prop} (m n : Nat), (ā (n : Nat), P 0 n) ā (ā (m n : Nat), 0 < m ā P (n % m) m ā P m n) ā P m ngcd.induction {P: Nat ā Nat ā PropP : Nat: TypeNat ā Nat: TypeNat ā Prop: TypeProp} (m: Natm n: Natn : Nat: TypeNat)
(H0: ā (n : Nat), P 0 nH0 : ān: ?m.327n, P: Nat ā Nat ā PropP 0: ?m.3310 n: ?m.327n) (H1: ā (m n : Nat), 0 < m ā P (n % m) m ā P m nH1 : ā m: ?m.342m n: ?m.345n, 0: ?m.3510 < m: ?m.342m ā P: Nat ā Nat ā PropP (n: ?m.345n % m: ?m.342m) m: ?m.342m ā P: Nat ā Nat ā PropP m: ?m.342m n: ?m.345n) : P: Nat ā Nat ā PropP m: Natm n: Natn :=
Nat.strongInductionOn: ā {motive : Nat ā Sort ?u.455} (n : Nat), (ā (n : Nat), (ā (m : Nat), m < n ā motive m) ā motive n) ā motive nNat.strongInductionOn (motive := fun m: ?m.457m => ā n: ?m.460n, P: Nat ā Nat ā PropP m: ?m.457m n: ?m.460n) m: Natm
(fun
| 0: Nat0, _ => H0: ā (n : Nat), P 0 nH0
| _+1, IH: ā (m : Nat), m < nā + 1 ā (fun m => ā (n : Nat), P m n) mIH => fun _: ?m.615_ => H1: ā (m n : Nat), 0 < m ā P (n % m) m ā P m nH1 _: Nat_ _: Nat_ (succ_pos: ā (n : Nat), 0 < succ nsucc_pos _: Nat_) (IH: ā (m : Nat), m < nā + 1 ā (fun m => ā (n : Nat), P m n) mIH _: Nat_ (mod_lt: ā (x : Nat) {y : Nat}, y > 0 ā x % y < ymod_lt _: Nat_ (succ_pos: ā (n : Nat), 0 < succ nsucc_pos _: Nat_)) _: Nat_) )
n: Natn

/-- The least common multiple of `m` and `n`, defined using `gcd`. -/
def lcm: Nat ā Nat ā Natlcm (m: Natm n: Natn : Nat: TypeNat) : Nat: TypeNat := m: Natm * n: Natn / gcd: Nat ā Nat ā Natgcd m: Natm n: Natn

/-- `m` and `n` are coprime, or relatively prime, if their `gcd` is 1. -/
@[reducible] def coprime: Nat ā Nat ā Propcoprime (m: Natm n: Natn : Nat: TypeNat) : Prop: TypeProp := gcd: Nat ā Nat ā Natgcd m: Natm n: Natn = 1: ?m.11581

---

theorem gcd_dvd: ā (m n : Nat), gcd m n ā£ m ā§ gcd m n ā£ ngcd_dvd (m: Natm n: Natn : Nat: TypeNat) : (gcd: Nat ā Nat ā Natgcd m: Natm n: Natn ā£ m: Natm) ā§ (gcd: Nat ā Nat ā Natgcd m: Natm n: Natn ā£ n: Natn) := byGoals accomplished! š
m, n: Natgcd m n ā£ m ā§ gcd m n ā£ ninduction m: Natm, n: Natn using gcd.induction: ā {P : Nat ā Nat ā Prop} (m n : Nat), (ā (n : Nat), P 0 n) ā (ā (m n : Nat), 0 < m ā P (n % m) m ā P m n) ā P m ngcd.induction with
m, n: Natgcd m n ā£ m ā§ gcd m n ā£ n| H0 n: Natn => n: NatH0gcd 0 n ā£ 0 ā§ gcd 0 n ā£ nrw [n: NatH0gcd 0 n ā£ 0 ā§ gcd 0 n ā£ ngcd_zero_left: ā (y : Nat), gcd 0 y = ygcd_zero_leftn: NatH0n ā£ 0 ā§ n ā£ n]n: NatH0n ā£ 0 ā§ n ā£ n;n: NatH0n ā£ 0 ā§ n ā£ n n: NatH0gcd 0 n ā£ 0 ā§ gcd 0 n ā£ nexact āØNat.dvd_zero: ā (a : Nat), a ā£ 0Nat.dvd_zero n: Natn, Nat.dvd_refl: ā (a : Nat), a ā£ aNat.dvd_refl n: Natnā©Goals accomplished! š
m, n: Natgcd m n ā£ m ā§ gcd m n ā£ n| H1 m: Natm n: Natn _: 0 < m_ IH: ?m.1213 (n % m) mIH => m, n: Nataā: 0 < mIH: gcd (n % m) m ā£ n % m ā§ gcd (n % m) m ā£ mH1gcd m n ā£ m ā§ gcd m n ā£ nrw [m, n: Nataā: 0 < mIH: gcd (n % m) m ā£ n % m ā§ gcd (n % m) m ā£ mH1gcd m n ā£ m ā§ gcd m n ā£ nā gcd_rec: ā (m n : Nat), gcd m n = gcd (n % m) mgcd_recm, n: Nataā: 0 < mIH: gcd m n ā£ n % m ā§ gcd m n ā£ mH1gcd m n ā£ m ā§ gcd m n ā£ n]m, n: Nataā: 0 < mIH: gcd m n ā£ n % m ā§ gcd m n ā£ mH1gcd m n ā£ m ā§ gcd m n ā£ n at IH: ?m.1213 (n % m) mIHm, n: Nataā: 0 < mIH: gcd m n ā£ n % m ā§ gcd m n ā£ mH1gcd m n ā£ m ā§ gcd m n ā£ n;m, n: Nataā: 0 < mIH: gcd m n ā£ n % m ā§ gcd m n ā£ mH1gcd m n ā£ m ā§ gcd m n ā£ n m, n: Nataā: 0 < mIH: gcd (n % m) m ā£ n % m ā§ gcd (n % m) m ā£ mH1gcd m n ā£ m ā§ gcd m n ā£ nexact āØIH: gcd m n ā£ n % m ā§ gcd m n ā£ mIH.2: ā {a b : Prop}, a ā§ b ā b2, (dvd_mod_iff: ā {k m n : Nat}, k ā£ n ā (k ā£ m % n ā k ā£ m)dvd_mod_iff IH: gcd m n ā£ n % m ā§ gcd m n ā£ mIH.2: ā {a b : Prop}, a ā§ b ā b2).1: ā {a b : Prop}, (a ā b) ā a ā b1 IH: gcd m n ā£ n % m ā§ gcd m n ā£ mIH.1: ā {a b : Prop}, a ā§ b ā a1ā©Goals accomplished! š

theorem gcd_dvd_left: ā (m n : Nat), gcd m n ā£ mgcd_dvd_left (m: Natm n: Natn : Nat: TypeNat) : gcd: Nat ā Nat ā Natgcd m: Natm n: Natn ā£ m: Natm := (gcd_dvd: ā (m n : Nat), gcd m n ā£ m ā§ gcd m n ā£ ngcd_dvd m: Natm n: Natn).left: ā {a b : Prop}, a ā§ b ā aleft

theorem gcd_dvd_right: ā (m n : Nat), gcd m n ā£ ngcd_dvd_right (m: Natm n: Natn : Nat: TypeNat) : gcd: Nat ā Nat ā Natgcd m: Natm n: Natn ā£ n: Natn := (gcd_dvd: ā (m n : Nat), gcd m n ā£ m ā§ gcd m n ā£ ngcd_dvd m: Natm n: Natn).right: ā {a b : Prop}, a ā§ b ā bright

theorem gcd_le_left: ā {m : Nat} (n : Nat), 0 < m ā gcd m n ā¤ mgcd_le_left (n: ?m.1383n) (h: 0 < mh : 0: ?m.13880 < m: ?m.1380m) : gcd: Nat ā Nat ā Natgcd m: ?m.1380m n: ?m.1383n ā¤ m: ?m.1380m := le_of_dvd: ā {m n : Nat}, 0 < n ā m ā£ n ā m ā¤ nle_of_dvd h: 0 < mh <| gcd_dvd_left: ā (m n : Nat), gcd m n ā£ mgcd_dvd_left m: Natm n: Natn

theorem gcd_le_right: ā {m : Nat} (n : Nat), 0 < n ā gcd m n ā¤ ngcd_le_right (n: ?m.1513n) (h: 0 < nh : 0: ?m.15180 < n: ?m.1513n) : gcd: Nat ā Nat ā Natgcd m: ?m.1510m n: ?m.1513n ā¤ n: ?m.1513n := le_of_dvd: ā {m n : Nat}, 0 < n ā m ā£ n ā m ā¤ nle_of_dvd h: 0 < nh <| gcd_dvd_right: ā (m n : Nat), gcd m n ā£ ngcd_dvd_right m: Natm n: Natn

theorem dvd_gcd: ā {k m n : Nat}, k ā£ m ā k ā£ n ā k ā£ gcd m ndvd_gcd : k: ?m.1599k ā£ m: ?m.1609m ā k: ?m.1599k ā£ n: ?m.1629n ā k: ?m.1599k ā£ gcd: Nat ā Nat ā Natgcd m: ?m.1609m n: ?m.1629n := byGoals accomplished! š
k, m, n: Natk ā£ m ā k ā£ n ā k ā£ gcd m ninduction m: Natm, n: Natn using gcd.induction: ā {P : Nat ā Nat ā Prop} (m n : Nat), (ā (n : Nat), P 0 n) ā (ā (m n : Nat), 0 < m ā P (n % m) m ā P m n) ā P m ngcd.induction with k, m, n: Natk ā£ m ā k ā£ n ā k ā£ gcd m nintro km: k ā£ 0km kn: k ā£ mknk, n, m: Nataā: 0 < nIH: k ā£ m % n ā k ā£ n ā k ā£ gcd (m % n) nkm: k ā£ nkn: k ā£ mH1k ā£ gcd n m
k, m, n: Natk ā£ m ā k ā£ n ā k ā£ gcd m n| H0 n: Natn => k, n: Natkm: k ā£ 0kn: k ā£ nH0k ā£ gcd 0 nrw [k, n: Natkm: k ā£ 0kn: k ā£ nH0k ā£ gcd 0 ngcd_zero_left: ā (y : Nat), gcd 0 y = ygcd_zero_leftk, n: Natkm: k ā£ 0kn: k ā£ nH0k ā£ n]k, n: Natkm: k ā£ 0kn: k ā£ nH0k ā£ n;k, n: Natkm: k ā£ 0kn: k ā£ nH0k ā£ n k, n: Natkm: k ā£ 0kn: k ā£ nH0k ā£ gcd 0 nexact kn: k ā£ nknGoals accomplished! š
k, m, n: Natk ā£ m ā k ā£ n ā k ā£ gcd m n| H1 n: Natn m: Natm _: 0 < n_ IH: ?m.1685 (m % n) nIH => k, n, m: Nataā: 0 < nIH: k ā£ m % n ā k ā£ n ā k ā£ gcd (m % n) nkm: k ā£ nkn: k ā£ mH1k ā£ gcd n mrw [k, n, m: Nataā: 0 < nIH: k ā£ m % n ā k ā£ n ā k ā£ gcd (m % n) nkm: k ā£ nkn: k ā£ mH1k ā£ gcd n mgcd_rec: ā (m n : Nat), gcd m n = gcd (n % m) mgcd_reck, n, m: Nataā: 0 < nIH: k ā£ m % n ā k ā£ n ā k ā£ gcd (m % n) nkm: k ā£ nkn: k ā£ mH1k ā£ gcd (m % n) n]k, n, m: Nataā: 0 < nIH: k ā£ m % n ā k ā£ n ā k ā£ gcd (m % n) nkm: k ā£ nkn: k ā£ mH1k ā£ gcd (m % n) n;k, n, m: Nataā: 0 < nIH: k ā£ m % n ā k ā£ n ā k ā£ gcd (m % n) nkm: k ā£ nkn: k ā£ mH1k ā£ gcd (m % n) n k, n, m: Nataā: 0 < nIH: k ā£ m % n ā k ā£ n ā k ā£ gcd (m % n) nkm: k ā£ nkn: k ā£ mH1k ā£ gcd n mexact IH: ?m.1685 (m % n) nIH ((dvd_mod_iff: ā {k m n : Nat}, k ā£ n ā (k ā£ m % n ā k ā£ m)dvd_mod_iff km: k ā£ nkm).2: ā {a b : Prop}, (a ā b) ā b ā a2 kn: k ā£ mkn) km: k ā£ nkmGoals accomplished! š

theorem dvd_gcd_iff: ā {k : Nat} {m n : Nat}, k ā£ gcd m n ā k ā£ m ā§ k ā£ ndvd_gcd_iff : k: ?m.1788k ā£ gcd: Nat ā Nat ā Natgcd m: ?m.1795m n: ?m.1802n ā k: ?m.1788k ā£ m: ?m.1795m ā§ k: ?m.1788k ā£ n: ?m.1802n :=
āØfun h: ?m.1829h => let āØhā: gcd m n ā£ mhā, hā: gcd m n ā£ nhāā© := gcd_dvd: ā (m n : Nat), gcd m n ā£ m ā§ gcd m n ā£ ngcd_dvd m: Natm n: Natn; āØNat.dvd_trans: ā {a b c : Nat}, a ā£ b ā b ā£ c ā a ā£ cNat.dvd_trans h: ?m.1829h hā: gcd m n ā£ mhā, Nat.dvd_trans: ā {a b c : Nat}, a ā£ b ā b ā£ c ā a ā£ cNat.dvd_trans h: ?m.1829h hā: gcd m n ā£ nhāā©,
fun āØhā: k ā£ mhā, hā: k ā£ nhāā© => dvd_gcd: ā {k m n : Nat}, k ā£ m ā k ā£ n ā k ā£ gcd m ndvd_gcd hā: k ā£ mhā hā: k ā£ nhāā©

theorem gcd_comm: ā (m n : Nat), gcd m n = gcd n mgcd_comm (m: Natm n: Natn : Nat: TypeNat) : gcd: Nat ā Nat ā Natgcd m: Natm n: Natn = gcd: Nat ā Nat ā Natgcd n: Natn m: Natm :=
dvd_antisymm: ā {m n : Nat}, m ā£ n ā n ā£ m ā m = ndvd_antisymm
(dvd_gcd: ā {k m n : Nat}, k ā£ m ā k ā£ n ā k ā£ gcd m ndvd_gcd (gcd_dvd_right: ā (m n : Nat), gcd m n ā£ ngcd_dvd_right m: Natm n: Natn) (gcd_dvd_left: ā (m n : Nat), gcd m n ā£ mgcd_dvd_left m: Natm n: Natn))
(dvd_gcd: ā {k m n : Nat}, k ā£ m ā k ā£ n ā k ā£ gcd m ndvd_gcd (gcd_dvd_right: ā (m n : Nat), gcd m n ā£ ngcd_dvd_right n: Natn m: Natm) (gcd_dvd_left: ā (m n : Nat), gcd m n ā£ mgcd_dvd_left n: Natn m: Natm))

theorem gcd_eq_left_iff_dvd: ā {m n : Nat}, m ā£ n ā gcd m n = mgcd_eq_left_iff_dvd : m: ?m.2071m ā£ n: ?m.2078n ā gcd: Nat ā Nat ā Natgcd m: ?m.2071m n: ?m.2078n = m: ?m.2071m :=
āØfun h: ?m.2105h => byGoals accomplished! š m, n: Nath: m ā£ ngcd m n = mrw [m, n: Nath: m ā£ ngcd m n = mgcd_rec: ā (m n : Nat), gcd m n = gcd (n % m) mgcd_rec,m, n: Nath: m ā£ ngcd (n % m) m = m m, n: Nath: m ā£ ngcd m n = mmod_eq_zero_of_dvd: ā {m n : Nat}, m ā£ n ā n % m = 0mod_eq_zero_of_dvd h: m ā£ nh,m, n: Nath: m ā£ ngcd 0 m = m m, n: Nath: m ā£ ngcd m n = mgcd_zero_left: ā (y : Nat), gcd 0 y = ygcd_zero_leftm, n: Nath: m ā£ nm = m]Goals accomplished! š,
fun h: ?m.2112h => h: ?m.2112h āø gcd_dvd_right: ā (m n : Nat), gcd m n ā£ ngcd_dvd_right m: Natm n: Natnā©

theorem gcd_eq_right_iff_dvd: ā {m n : Nat}, m ā£ n ā gcd n m = mgcd_eq_right_iff_dvd : m: ?m.2165m ā£ n: ?m.2172n ā gcd: Nat ā Nat ā Natgcd n: ?m.2172n m: ?m.2165m = m: ?m.2165m := byGoals accomplished! š
m, n: Natm ā£ n ā gcd n m = mrw [m, n: Natm ā£ n ā gcd n m = mgcd_comm: ā (m n : Nat), gcd m n = gcd n mgcd_commm, n: Natm ā£ n ā gcd m n = m]m, n: Natm ā£ n ā gcd m n = m;m, n: Natm ā£ n ā gcd m n = m m, n: Natm ā£ n ā gcd n m = mexact gcd_eq_left_iff_dvd: ā {m n : Nat}, m ā£ n ā gcd m n = mgcd_eq_left_iff_dvdGoals accomplished! š

theorem gcd_assoc: ā (m n k : Nat), gcd (gcd m n) k = gcd m (gcd n k)gcd_assoc (m: Natm n: Natn k: Natk : Nat: TypeNat) : gcd: Nat ā Nat ā Natgcd (gcd: Nat ā Nat ā Natgcd m: Natm n: Natn) k: Natk = gcd: Nat ā Nat ā Natgcd m: Natm (gcd: Nat ā Nat ā Natgcd n: Natn k: Natk) :=
dvd_antisymm: ā {m n : Nat}, m ā£ n ā n ā£ m ā m = ndvd_antisymm
(dvd_gcd: ā {k m n : Nat}, k ā£ m ā k ā£ n ā k ā£ gcd m ndvd_gcd
(Nat.dvd_trans: ā {a b c : Nat}, a ā£ b ā b ā£ c ā a ā£ cNat.dvd_trans (gcd_dvd_left: ā (m n : Nat), gcd m n ā£ mgcd_dvd_left (gcd: Nat ā Nat ā Natgcd m: Natm n: Natn) k: Natk) (gcd_dvd_left: ā (m n : Nat), gcd m n ā£ mgcd_dvd_left m: Natm n: Natn))
(dvd_gcd: ā {k m n : Nat}, k ā£ m ā k ā£ n ā k ā£ gcd m ndvd_gcd (Nat.dvd_trans: ā {a b c : Nat}, a ā£ b ā b ā£ c ā a ā£ cNat.dvd_trans (gcd_dvd_left: ā (m n : Nat), gcd m n ā£ mgcd_dvd_left (gcd: Nat ā Nat ā Natgcd m: Natm n: Natn) k: Natk) (gcd_dvd_right: ā (m n : Nat), gcd m n ā£ ngcd_dvd_right m: Natm n: Natn))
(gcd_dvd_right: ā (m n : Nat), gcd m n ā£ ngcd_dvd_right (gcd: Nat ā Nat ā Natgcd m: Natm n: Natn) k: Natk)))
(dvd_gcd: ā {k m n : Nat}, k ā£ m ā k ā£ n ā k ā£ gcd m ndvd_gcd
(dvd_gcd: ā {k m n : Nat}, k ā£ m ā k ā£ n ā k ā£ gcd m ndvd_gcd (gcd_dvd_left: ā (m n : Nat), gcd m n ā£ mgcd_dvd_left m: Natm (gcd: Nat ā Nat ā Natgcd n: Natn k: Natk))
(Nat.dvd_trans: ā {a b c : Nat}, a ā£ b ā b ā£ c ā a ā£ cNat.dvd_trans (gcd_dvd_right: ā (m n : Nat), gcd m n ā£ ngcd_dvd_right m: Natm (gcd: Nat ā Nat ā Natgcd n: Natn k: Natk)) (gcd_dvd_left: ā (m n : Nat), gcd m n ā£ mgcd_dvd_left n: Natn k: Natk)))
(Nat.dvd_trans: ā {a b c : Nat}, a ā£ b ā b ā£ c ā a ā£ cNat.dvd_trans (gcd_dvd_right: ā (m n : Nat), gcd m n ā£ ngcd_dvd_right m: Natm (gcd: Nat ā Nat ā Natgcd n: Natn k: Natk)) (gcd_dvd_right: ā (m n : Nat), gcd m n ā£ ngcd_dvd_right n: Natn k: Natk)))

@[simp] theorem gcd_one_right: ā (n : Nat), gcd n 1 = 1gcd_one_right (n: Natn : Nat: TypeNat) : gcd: Nat ā Nat ā Natgcd n: Natn 1: ?m.22801 = 1: ?m.22891 := (gcd_comm: ā (m n : Nat), gcd m n = gcd n mgcd_comm n: Natn 1: ?m.23061).trans: ā {Ī± : Sort ?u.2308} {a b c : Ī±}, a = b ā b = c ā a = ctrans (gcd_one_left: ā (n : Nat), gcd 1 n = 1gcd_one_left n: Natn)

theorem gcd_mul_left: ā (m n k : Nat), gcd (m * n) (m * k) = m * gcd n kgcd_mul_left (m: Natm n: Natn k: Natk : Nat: TypeNat) : gcd: Nat ā Nat ā Natgcd (m: Natm * n: Natn) (m: Natm * k: Natk) = m: Natm * gcd: Nat ā Nat ā Natgcd n: Natn k: Natk := byGoals accomplished! š
m, n, k: Natgcd (m * n) (m * k) = m * gcd n kinduction n: Natn, k: Natk using gcd.induction: ā {P : Nat ā Nat ā Prop} (m n : Nat), (ā (n : Nat), P 0 n) ā (ā (m n : Nat), 0 < m ā P (n % m) m ā P m n) ā P m ngcd.induction with
m, n, k: Natgcd (m * n) (m * k) = m * gcd n k| H0 k: Natk => m, k: NatH0gcd (m * 0) (m * k) = m * gcd 0 ksimpGoals accomplished! š
m, n, k: Natgcd (m * n) (m * k) = m * gcd n k| H1 n: Natn k: Natk _: 0 < n_ IH: ?m.2444 (k % n) nIH => m, n, k: Nataā: 0 < nIH: gcd (m * (k % n)) (m * n) = m * gcd (k % n) nH1gcd (m * n) (m * k) = m * gcd n krwa [m, n, k: Nataā: 0 < nIH: gcd (m * (k % n)) (m * n) = m * gcd (k % n) nH1gcd (m * n) (m * k) = m * gcd n kā mul_mod_mul_left: ā (z x y : Nat), z * x % (z * y) = z * (x % y)mul_mod_mul_left,m, n, k: Nataā: 0 < nIH: gcd (m * k % (m * n)) (m * n) = m * gcd (k % n) nH1gcd (m * n) (m * k) = m * gcd n k m, n, k: Nataā: 0 < nIH: gcd (m * (k % n)) (m * n) = m * gcd (k % n) nH1gcd (m * n) (m * k) = m * gcd n kā gcd_rec: ā (m n : Nat), gcd m n = gcd (n % m) mgcd_rec,m, n, k: Nataā: 0 < nIH: gcd (m * n) (m * k) = m * gcd (k % n) nH1gcd (m * n) (m * k) = m * gcd n k m, n, k: Nataā: 0 < nIH: gcd (m * (k % n)) (m * n) = m * gcd (k % n) nH1gcd (m * n) (m * k) = m * gcd n kā gcd_rec: ā (m n : Nat), gcd m n = gcd (n % m) mgcd_recm, n, k: Nataā: 0 < nIH: gcd (m * n) (m * k) = m * gcd n kH1gcd (m * n) (m * k) = m * gcd n k]m, n, k: Nataā: 0 < nIH: gcd (m * n) (m * k) = m * gcd n kH1gcd (m * n) (m * k) = m * gcd n k at IH: gcd (m * k % (m * n)) (m * n) = m * gcd (k % n) nIHGoals accomplished! š

theorem gcd_mul_right: ā (m n k : Nat), gcd (m * n) (k * n) = gcd m k * ngcd_mul_right (m: Natm n: Natn k: Natk : Nat: TypeNat) : gcd: Nat ā Nat ā Natgcd (m: Natm * n: Natn) (k: Natk * n: Natn) = gcd: Nat ā Nat ā Natgcd m: Natm k: Natk * n: Natn := byGoals accomplished! š
m, n, k: Natgcd (m * n) (k * n) = gcd m k * nrw [m, n, k: Natgcd (m * n) (k * n) = gcd m k * nNat.mul_comm: ā (n m : Nat), n * m = m * nNat.mul_comm m: Natm n: Natn,m, n, k: Natgcd (n * m) (k * n) = gcd m k * n m, n, k: Natgcd (m * n) (k * n) = gcd m k * nNat.mul_comm: ā (n m : Nat), n * m = m * nNat.mul_comm k: Natk n: Natn,m, n, k: Natgcd (n * m) (n * k) = gcd m k * n m, n, k: Natgcd (m * n) (k * n) = gcd m k * nNat.mul_comm: ā (n m : Nat), n * m = m * nNat.mul_comm (gcd: Nat ā Nat ā Natgcd m: Natm k: Natk) n: Natn,m, n, k: Natgcd (n * m) (n * k) = n * gcd m k m, n, k: Natgcd (m * n) (k * n) = gcd m k * ngcd_mul_left: ā (m n k : Nat), gcd (m * n) (m * k) = m * gcd n kgcd_mul_leftm, n, k: Natn * gcd m k = n * gcd m k]Goals accomplished! š

theorem gcd_pos_of_pos_left: ā {m : Nat} (n : Nat), 0 < m ā 0 < gcd m ngcd_pos_of_pos_left {m: Natm : Nat: TypeNat} (n: Natn : Nat: TypeNat) (mpos: 0 < mmpos : 0: ?m.27470 < m: Natm) : 0: ?m.27750 < gcd: Nat ā Nat ā Natgcd m: Natm n: Natn :=
pos_of_dvd_of_pos: ā {m n : Nat}, m ā£ n ā 0 < n ā 0 < mpos_of_dvd_of_pos (gcd_dvd_left: ā (m n : Nat), gcd m n ā£ mgcd_dvd_left m: Natm n: Natn) mpos: 0 < mmpos

theorem gcd_pos_of_pos_right: ā (m : Nat) {n : Nat}, 0 < n ā 0 < gcd m ngcd_pos_of_pos_right (m: Natm : Nat: TypeNat) {n: Natn : Nat: TypeNat} (npos: 0 < nnpos : 0: ?m.28180 < n: Natn) : 0: ?m.28460 < gcd: Nat ā Nat ā Natgcd m: Natm n: Natn :=
pos_of_dvd_of_pos: ā {m n : Nat}, m ā£ n ā 0 < n ā 0 < mpos_of_dvd_of_pos (gcd_dvd_right: ā (m n : Nat), gcd m n ā£ ngcd_dvd_right m: Natm n: Natn) npos: 0 < nnpos

theorem div_gcd_pos_of_pos_left: ā {a : Nat} (b : Nat), 0 < a ā 0 < a / gcd a bdiv_gcd_pos_of_pos_left (b: Natb : Nat: TypeNat) (h: 0 < ah : 0: ?m.29060 < a: ?m.2899a) : 0: ?m.29490 < a: ?m.2899a / a: ?m.2899a.gcd: Nat ā Nat ā Natgcd b: Natb :=
(Nat.le_div_iff_mul_le: ā {k x y : Nat}, 0 < k ā (x ā¤ y / k ā x * k ā¤ y)Nat.le_div_iff_mul_le <| Nat.gcd_pos_of_pos_left: ā {m : Nat} (n : Nat), 0 < m ā 0 < gcd m nNat.gcd_pos_of_pos_left _: Nat_ h: 0 < ah).2: ā {a b : Prop}, (a ā b) ā b ā a2 (Nat.one_mul: ā (n : Nat), 1 * n = nNat.one_mul _: Nat_ āø Nat.gcd_le_left: ā {m : Nat} (n : Nat), 0 < m ā gcd m n ā¤ mNat.gcd_le_left _: Nat_ h: 0 < ah)

theorem div_gcd_pos_of_pos_right: ā {b : Nat} (a : Nat), 0 < b ā 0 < b / gcd a bdiv_gcd_pos_of_pos_right (a: Nata : Nat: TypeNat) (h: 0 < bh : 0: ?m.31730 < b: ?m.3166b) : 0: ?m.32160 < b: ?m.3166b / a: Nata.gcd: Nat ā Nat ā Natgcd b: ?m.3166b :=
(Nat.le_div_iff_mul_le: ā {k x y : Nat}, 0 < k ā (x ā¤ y / k ā x * k ā¤ y)Nat.le_div_iff_mul_le <| Nat.gcd_pos_of_pos_right: ā (m : Nat) {n : Nat}, 0 < n ā 0 < gcd m nNat.gcd_pos_of_pos_right _: Nat_ h: 0 < bh).2: ā {a b : Prop}, (a ā b) ā b ā a2 (Nat.one_mul: ā (n : Nat), 1 * n = nNat.one_mul _: Nat_ āø Nat.gcd_le_right: ā {m : Nat} (n : Nat), 0 < n ā gcd m n ā¤ nNat.gcd_le_right _: Nat_ h: 0 < bh)

theorem eq_zero_of_gcd_eq_zero_left: ā {m n : Nat}, gcd m n = 0 ā m = 0eq_zero_of_gcd_eq_zero_left {m: Natm n: Natn : Nat: TypeNat} (H: gcd m n = 0H : gcd: Nat ā Nat ā Natgcd m: Natm n: Natn = 0: ?m.33450) : m: Natm = 0: ?m.33670 :=
match eq_zero_or_pos: ā (n : Nat), n = 0 āØ n > 0eq_zero_or_pos m: Natm with
| .inl: ā {a b : Prop}, a ā a āØ b.inl H0: m = 0H0 => H0: m = 0H0
| .inr: ā {a b : Prop}, b ā a āØ b.inr H1: m > 0H1 => absurd: ā {a : Prop} {b : Sort ?u.3408}, a ā Ā¬a ā babsurd (Eq.symm: ā {Ī± : Sort ?u.3411} {a b : Ī±}, a = b ā b = aEq.symm H: gcd m n = 0H) (ne_of_lt: ā {a b : Nat}, a < b ā a ā  bne_of_lt (gcd_pos_of_pos_left: ā {m : Nat} (n : Nat), 0 < m ā 0 < gcd m ngcd_pos_of_pos_left _: Nat_ H1: m > 0H1))

theorem eq_zero_of_gcd_eq_zero_right: ā {m n : Nat}, gcd m n = 0 ā n = 0eq_zero_of_gcd_eq_zero_right {m: Natm n: Natn : Nat: TypeNat} (H: gcd m n = 0H : gcd: Nat ā Nat ā Natgcd m: Natm n: Natn = 0: ?m.35110) : n: Natn = 0: ?m.35330 := byGoals accomplished! š
m, n: NatH: gcd m n = 0n = 0rw [m, n: NatH: gcd m n = 0n = 0gcd_comm: ā (m n : Nat), gcd m n = gcd n mgcd_commm, n: NatH: gcd n m = 0n = 0]m, n: NatH: gcd n m = 0n = 0 at H: gcd m n = 0Hm, n: NatH: gcd n m = 0n = 0
m, n: NatH: gcd m n = 0n = 0exact eq_zero_of_gcd_eq_zero_left: ā {m n : Nat}, gcd m n = 0 ā m = 0eq_zero_of_gcd_eq_zero_left H: gcd n m = 0HGoals accomplished! š

theorem gcd_ne_zero_left: ā {m n : Nat}, m ā  0 ā gcd m n ā  0gcd_ne_zero_left : m: ?m.3590m ā  0: ?m.36170 ā gcd: Nat ā Nat ā Natgcd m: ?m.3590m n: ?m.3610n ā  0: ?m.36300 := mt: ā {a b : Prop}, (a ā b) ā Ā¬b ā Ā¬amt eq_zero_of_gcd_eq_zero_left: ā {m n : Nat}, gcd m n = 0 ā m = 0eq_zero_of_gcd_eq_zero_left

theorem gcd_ne_zero_right: ā {n m : Nat}, n ā  0 ā gcd m n ā  0gcd_ne_zero_right : n: ?m.3673n ā  0: ?m.37000 ā gcd: Nat ā Nat ā Natgcd m: ?m.3693m n: ?m.3673n ā  0: ?m.37130 := mt: ā {a b : Prop}, (a ā b) ā Ā¬b ā Ā¬amt eq_zero_of_gcd_eq_zero_right: ā {m n : Nat}, gcd m n = 0 ā n = 0eq_zero_of_gcd_eq_zero_right

theorem gcd_div: ā {m n k : Nat}, k ā£ m ā k ā£ n ā gcd (m / k) (n / k) = gcd m n / kgcd_div {m: Natm n: Natn k: Natk : Nat: TypeNat} (H1: k ā£ mH1 : k: Natk ā£ m: Natm) (H2: k ā£ nH2 : k: Natk ā£ n: Natn) :
gcd: Nat ā Nat ā Natgcd (m: Natm / k: Natk) (n: Natn / k: Natk) = gcd: Nat ā Nat ā Natgcd m: Natm n: Natn / k: Natk :=
match eq_zero_or_pos: ā (n : Nat), n = 0 āØ n > 0eq_zero_or_pos k: Natk with
| .inl: ā {a b : Prop}, a ā a āØ b.inl H0: k = 0H0 => byGoals accomplished! š m, n, k: NatH1: k ā£ mH2: k ā£ nH0: k = 0gcd (m / k) (n / k) = gcd m n / ksimp [H0: k = 0H0]Goals accomplished! š
| .inr: ā {a b : Prop}, b ā a āØ b.inr H3: k > 0H3 => byGoals accomplished! š
m, n, k: NatH1: k ā£ mH2: k ā£ nH3: k > 0gcd (m / k) (n / k) = gcd m n / kapply Nat.eq_of_mul_eq_mul_right: ā {n m k : Nat}, 0 < m ā n * m = k * m ā n = kNat.eq_of_mul_eq_mul_right H3: k > 0H3m, n, k: NatH1: k ā£ mH2: k ā£ nH3: k > 0gcd (m / k) (n / k) * k = gcd m n / k * k
m, n, k: NatH1: k ā£ mH2: k ā£ nH3: k > 0gcd (m / k) (n / k) = gcd m n / krw [m, n, k: NatH1: k ā£ mH2: k ā£ nH3: k > 0gcd (m / k) (n / k) * k = gcd m n / k * kNat.div_mul_cancel: ā {n m : Nat}, n ā£ m ā m / n * n = mNat.div_mul_cancel (dvd_gcd: ā {k m n : Nat}, k ā£ m ā k ā£ n ā k ā£ gcd m ndvd_gcd H1: k ā£ mH1 H2: k ā£ nH2),m, n, k: NatH1: k ā£ mH2: k ā£ nH3: k > 0gcd (m / k) (n / k) * k = gcd m n m, n, k: NatH1: k ā£ mH2: k ā£ nH3: k > 0gcd (m / k) (n / k) * k = gcd m n / k * kā gcd_mul_right: ā (m n k : Nat), gcd (m * n) (k * n) = gcd m k * ngcd_mul_right,m, n, k: NatH1: k ā£ mH2: k ā£ nH3: k > 0gcd (m / k * k) (n / k * k) = gcd m n
m, n, k: NatH1: k ā£ mH2: k ā£ nH3: k > 0gcd (m / k) (n / k) * k = gcd m n / k * kNat.div_mul_cancel: ā {n m : Nat}, n ā£ m ā m / n * n = mNat.div_mul_cancel H1: k ā£ mH1,m, n, k: NatH1: k ā£ mH2: k ā£ nH3: k > 0gcd m (n / k * k) = gcd m n m, n, k: NatH1: k ā£ mH2: k ā£ nH3: k > 0gcd (m / k) (n / k) * k = gcd m n / k * kNat.div_mul_cancel: ā {n m : Nat}, n ā£ m ā m / n * n = mNat.div_mul_cancel H2: k ā£ nH2m, n, k: NatH1: k ā£ mH2: k ā£ nH3: k > 0gcd m n = gcd m n]Goals accomplished! š

theorem gcd_dvd_gcd_of_dvd_left: ā {m k : Nat} (n : Nat), m ā£ k ā gcd m n ā£ gcd k ngcd_dvd_gcd_of_dvd_left {m: Natm k: Natk : Nat: TypeNat} (n: Natn : Nat: TypeNat) (H: m ā£ kH : m: Natm ā£ k: Natk) : gcd: Nat ā Nat ā Natgcd m: Natm n: Natn ā£ gcd: Nat ā Nat ā Natgcd k: Natk n: Natn :=
dvd_gcd: ā {k m n : Nat}, k ā£ m ā k ā£ n ā k ā£ gcd m ndvd_gcd (Nat.dvd_trans: ā {a b c : Nat}, a ā£ b ā b ā£ c ā a ā£ cNat.dvd_trans (gcd_dvd_left: ā (m n : Nat), gcd m n ā£ mgcd_dvd_left m: Natm n: Natn) H: m ā£ kH) (gcd_dvd_right: ā (m n : Nat), gcd m n ā£ ngcd_dvd_right m: Natm n: Natn)

theorem gcd_dvd_gcd_of_dvd_right: ā {m k : Nat} (n : Nat), m ā£ k ā gcd n m ā£ gcd n kgcd_dvd_gcd_of_dvd_right {m: Natm k: Natk : Nat: TypeNat} (n: Natn : Nat: TypeNat) (H: m ā£ kH : m: Natm ā£ k: Natk) : gcd: Nat ā Nat ā Natgcd n: Natn m: Natm ā£ gcd: Nat ā Nat ā Natgcd n: Natn k: Natk :=
dvd_gcd: ā {k m n : Nat}, k ā£ m ā k ā£ n ā k ā£ gcd m ndvd_gcd (gcd_dvd_left: ā (m n : Nat), gcd m n ā£ mgcd_dvd_left n: Natn m: Natm) (Nat.dvd_trans: ā {a b c : Nat}, a ā£ b ā b ā£ c ā a ā£ cNat.dvd_trans (gcd_dvd_right: ā (m n : Nat), gcd m n ā£ ngcd_dvd_right n: Natn m: Natm) H: m ā£ kH)

theorem gcd_dvd_gcd_mul_left: ā (m n k : Nat), gcd m n ā£ gcd (k * m) ngcd_dvd_gcd_mul_left (m: Natm n: Natn k: Natk : Nat: TypeNat) : gcd: Nat ā Nat ā Natgcd m: Natm n: Natn ā£ gcd: Nat ā Nat ā Natgcd (k: Natk * m: Natm) n: Natn :=
gcd_dvd_gcd_of_dvd_left: ā {m k : Nat} (n : Nat), m ā£ k ā gcd m n ā£ gcd k ngcd_dvd_gcd_of_dvd_left _: Nat_ (Nat.dvd_mul_left: ā (a b : Nat), a ā£ b * aNat.dvd_mul_left _: Nat_ _: Nat_)

theorem gcd_dvd_gcd_mul_right: ā (m n k : Nat), gcd m n ā£ gcd (m * k) ngcd_dvd_gcd_mul_right (m: Natm n: Natn k: Natk : Nat: TypeNat) : gcd: Nat ā Nat ā Natgcd m: Natm n: Natn ā£ gcd: Nat ā Nat ā Natgcd (m: Natm * k: Natk) n: Natn :=
gcd_dvd_gcd_of_dvd_left: ā {m k : Nat} (n : Nat), m ā£ k ā gcd m n ā£ gcd k ngcd_dvd_gcd_of_dvd_left _: Nat_ (Nat.dvd_mul_right: ā (a b : Nat), a ā£ a * bNat.dvd_mul_right _: Nat_ _: Nat_)

theorem gcd_dvd_gcd_mul_left_right: ā (m n k : Nat), gcd m n ā£ gcd m (k * n)gcd_dvd_gcd_mul_left_right (m: Natm n: Natn k: Natk : Nat: TypeNat) : gcd: Nat ā Nat ā Natgcd m: Natm n: Natn ā£ gcd: Nat ā Nat ā Natgcd m: Natm (k: Natk * n: Natn) :=
gcd_dvd_gcd_of_dvd_right: ā {m k : Nat} (n : Nat), m ā£ k ā gcd n m ā£ gcd n kgcd_dvd_gcd_of_dvd_right _: Nat_ (Nat.dvd_mul_left: ā (a b : Nat), a ā£ b * aNat.dvd_mul_left _: Nat_ _: Nat_)

theorem gcd_dvd_gcd_mul_right_right: ā (m n k : Nat), gcd m n ā£ gcd m (n * k)gcd_dvd_gcd_mul_right_right (m: Natm n: Natn k: Natk : Nat: TypeNat) : gcd: Nat ā Nat ā Natgcd m: Natm n: Natn ā£ gcd: Nat ā Nat ā Natgcd m: Natm (n: Natn * k: Natk) :=
gcd_dvd_gcd_of_dvd_right: ā {m k : Nat} (n : Nat), m ā£ k ā gcd n m ā£ gcd n kgcd_dvd_gcd_of_dvd_right _: Nat_ (Nat.dvd_mul_right: ā (a b : Nat), a ā£ a * bNat.dvd_mul_right _: Nat_ _: Nat_)

theorem gcd_eq_left: ā {m n : Nat}, m ā£ n ā gcd m n = mgcd_eq_left {m: Natm n: Natn : Nat: TypeNat} (H: m ā£ nH : m: Natm ā£ n: Natn) : gcd: Nat ā Nat ā Natgcd m: Natm n: Natn = m: Natm :=
dvd_antisymm: ā {m n : Nat}, m ā£ n ā n ā£ m ā m = ndvd_antisymm (gcd_dvd_left: ā (m n : Nat), gcd m n ā£ mgcd_dvd_left _: Nat_ _: Nat_) (dvd_gcd: ā {k m n : Nat}, k ā£ m ā k ā£ n ā k ā£ gcd m ndvd_gcd (Nat.dvd_refl: ā (a : Nat), a ā£ aNat.dvd_refl _: Nat_) H: m ā£ nH)

theorem gcd_eq_right: ā {m n : Nat}, n ā£ m ā gcd m n = ngcd_eq_right {m: Natm n: Natn : Nat: TypeNat} (H: n ā£ mH : n: Natn ā£ m: Natm) : gcd: Nat ā Nat ā Natgcd m: Natm n: Natn = n: Natn := byGoals accomplished! š
m, n: NatH: n ā£ mgcd m n = nrw [m, n: NatH: n ā£ mgcd m n = ngcd_comm: ā (m n : Nat), gcd m n = gcd n mgcd_comm,m, n: NatH: n ā£ mgcd n m = n m, n: NatH: n ā£ mgcd m n = ngcd_eq_left: ā {m n : Nat}, m ā£ n ā gcd m n = mgcd_eq_left H: n ā£ mHm, n: NatH: n ā£ mn = n]Goals accomplished! š

@[simp] theorem gcd_mul_left_left: ā (m n : Nat), gcd (m * n) n = ngcd_mul_left_left (m: Natm n: Natn : Nat: TypeNat) : gcd: Nat ā Nat ā Natgcd (m: Natm * n: Natn) n: Natn = n: Natn :=
dvd_antisymm: ā {m n : Nat}, m ā£ n ā n ā£ m ā m = ndvd_antisymm (gcd_dvd_right: ā (m n : Nat), gcd m n ā£ ngcd_dvd_right _: Nat_ _: Nat_) (dvd_gcd: ā {k m n : Nat}, k ā£ m ā k ā£ n ā k ā£ gcd m ndvd_gcd (Nat.dvd_mul_left: ā (a b : Nat), a ā£ b * aNat.dvd_mul_left _: Nat_ _: Nat_) (Nat.dvd_refl: ā (a : Nat), a ā£ aNat.dvd_refl _: Nat_))

@[simp] theorem gcd_mul_left_right: ā (m n : Nat), gcd n (m * n) = ngcd_mul_left_right (m: Natm n: Natn : Nat: TypeNat) : gcd: Nat ā Nat ā Natgcd n: Natn (m: Natm * n: Natn) = n: Natn := byGoals accomplished! š
m, n: Natgcd n (m * n) = nrw [m, n: Natgcd n (m * n) = ngcd_comm: ā (m n : Nat), gcd m n = gcd n mgcd_comm,m, n: Natgcd (m * n) n = n m, n: Natgcd n (m * n) = ngcd_mul_left_left: ā (m n : Nat), gcd (m * n) n = ngcd_mul_left_leftm, n: Natn = n]Goals accomplished! š

@[simp] theorem gcd_mul_right_left: ā (m n : Nat), gcd (n * m) n = ngcd_mul_right_left (m: Natm n: Natn : Nat: TypeNat) : gcd: Nat ā Nat ā Natgcd (n: Natn * m: Natm) n: Natn = n: Natn := byGoals accomplished! š
m, n: Natgcd (n * m) n = nrw [m, n: Natgcd (n * m) n = nNat.mul_comm: ā (n m : Nat), n * m = m * nNat.mul_comm,m, n: Natgcd (m * n) n = n m, n: Natgcd (n * m) n = ngcd_mul_left_left: ā (m n : Nat), gcd (m * n) n = ngcd_mul_left_leftm, n: Natn = n]Goals accomplished! š

@[simp] theorem gcd_mul_right_right: ā (m n : Nat), gcd n (n * m) = ngcd_mul_right_right (m: Natm n: Natn : Nat: TypeNat) : gcd: Nat ā Nat ā Natgcd n: Natn (n: Natn * m: Natm) = n: Natn := byGoals accomplished! š
m, n: Natgcd n (n * m) = nrw [m, n: Natgcd n (n * m) = ngcd_comm: ā (m n : Nat), gcd m n = gcd n mgcd_comm,m, n: Natgcd (n * m) n = n m, n: Natgcd n (n * m) = ngcd_mul_right_left: ā (m n : Nat), gcd (n * m) n = ngcd_mul_right_leftm, n: Natn = n]Goals accomplished! š

@[simp] theorem gcd_gcd_self_right_left: ā (m n : Nat), gcd m (gcd m n) = gcd m ngcd_gcd_self_right_left (m: Natm n: Natn : Nat: TypeNat) : gcd: Nat ā Nat ā Natgcd m: Natm (gcd: Nat ā Nat ā Natgcd m: Natm n: Natn) = gcd: Nat ā Nat ā Natgcd m: Natm n: Natn :=
dvd_antisymm: ā {m n : Nat}, m ā£ n ā n ā£ m ā m = ndvd_antisymm (gcd_dvd_right: ā (m n : Nat), gcd m n ā£ ngcd_dvd_right _: Nat_ _: Nat_) (dvd_gcd: ā {k m n : Nat}, k ā£ m ā k ā£ n ā k ā£ gcd m ndvd_gcd (gcd_dvd_left: ā (m n : Nat), gcd m n ā£ mgcd_dvd_left _: Nat_ _: Nat_) (Nat.dvd_refl: ā (a : Nat), a ā£ aNat.dvd_refl _: Nat_))

@[simp] theorem gcd_gcd_self_right_right: ā (m n : Nat), gcd m (gcd n m) = gcd n mgcd_gcd_self_right_right (m: Natm n: Natn : Nat: TypeNat) : gcd: Nat ā Nat ā Natgcd m: Natm (gcd: Nat ā Nat ā Natgcd n: Natn m: Natm) = gcd: Nat ā Nat ā Natgcd n: Natn m: Natm := byGoals accomplished! š
m, n: Natgcd m (gcd n m) = gcd n mrw [m, n: Natgcd m (gcd n m) = gcd n mgcd_comm: ā (m n : Nat), gcd m n = gcd n mgcd_comm n: Natn m: Natm,m, n: Natgcd m (gcd m n) = gcd m n m, n: Natgcd m (gcd n m) = gcd n mgcd_gcd_self_right_left: ā (m n : Nat), gcd m (gcd m n) = gcd m ngcd_gcd_self_right_leftm, n: Natgcd m n = gcd m n]Goals accomplished! š

@[simp] theorem gcd_gcd_self_left_right: ā (m n : Nat), gcd (gcd n m) m = gcd n mgcd_gcd_self_left_right (m: Natm n: Natn : Nat: TypeNat) : gcd: Nat ā Nat ā Natgcd (gcd: Nat ā Nat ā Natgcd n: Natn m: Natm) m: Natm = gcd: Nat ā Nat ā Natgcd n: Natn m: Natm := byGoals accomplished! š
m, n: Natgcd (gcd n m) m = gcd n mrw [m, n: Natgcd (gcd n m) m = gcd n mgcd_comm: ā (m n : Nat), gcd m n = gcd n mgcd_comm,m, n: Natgcd m (gcd n m) = gcd n m m, n: Natgcd (gcd n m) m = gcd n mgcd_gcd_self_right_right: ā (m n : Nat), gcd m (gcd n m) = gcd n mgcd_gcd_self_right_rightm, n: Natgcd n m = gcd n m]Goals accomplished! š

@[simp] theorem gcd_gcd_self_left_left: ā (m n : Nat), gcd (gcd m n) m = gcd m ngcd_gcd_self_left_left (m: Natm n: Natn : Nat: TypeNat) : gcd: Nat ā Nat ā Natgcd (gcd: Nat ā Nat ā Natgcd m: Natm n: Natn) m: Natm = gcd: Nat ā Nat ā Natgcd m: Natm n: Natn := byGoals accomplished! š
m, n: Natgcd (gcd m n) m = gcd m nrw [m, n: Natgcd (gcd m n) m = gcd m ngcd_comm: ā (m n : Nat), gcd m n = gcd n mgcd_comm m: Natm n: Natn,m, n: Natgcd (gcd n m) m = gcd n m m, n: Natgcd (gcd m n) m = gcd m ngcd_gcd_self_left_right: ā (m n : Nat), gcd (gcd n m) m = gcd n mgcd_gcd_self_left_rightm, n: Natgcd n m = gcd n m]Goals accomplished! š

theorem gcd_add_mul_self: ā (m n k : Nat), gcd m (n + k * m) = gcd m ngcd_add_mul_self (m: Natm n: Natn k: Natk : Nat: TypeNat) : gcd: Nat ā Nat ā Natgcd m: Natm (n: Natn + k: Natk * m: Natm) = gcd: Nat ā Nat ā Natgcd m: Natm n: Natn := byGoals accomplished! š
m, n, k: Natgcd m (n + k * m) = gcd m nsimp [gcd_rec: ā (m n : Nat), gcd m n = gcd (n % m) mgcd_rec m: Natm (n: Natn + k: Natk * m: Natm), gcd_rec: ā (m n : Nat), gcd m n = gcd (n % m) mgcd_rec m: Natm n: Natn]Goals accomplished! š

theorem gcd_eq_zero_iff: ā {i j : Nat}, gcd i j = 0 ā i = 0 ā§ j = 0gcd_eq_zero_iff {i: Nati j: Natj : Nat: TypeNat} : gcd: Nat ā Nat ā Natgcd i: Nati j: Natj = 0: ?m.53340 ā i: Nati = 0: ?m.53540 ā§ j: Natj = 0: ?m.53680 :=
āØfun h: ?m.5392h => āØeq_zero_of_gcd_eq_zero_left: ā {m n : Nat}, gcd m n = 0 ā m = 0eq_zero_of_gcd_eq_zero_left h: ?m.5392h, eq_zero_of_gcd_eq_zero_right: ā {m n : Nat}, gcd m n = 0 ā n = 0eq_zero_of_gcd_eq_zero_right h: ?m.5392hā©,
fun h: ?m.5414h => byGoals accomplished! š i, j: Nath: i = 0 ā§ j = 0gcd i j = 0simp [h: i = 0 ā§ j = 0h]Goals accomplished! šā©

/-! ### `lcm` -/

theorem lcm_comm: ā (m n : Nat), lcm m n = lcm n mlcm_comm (m: Natm n: Natn : Nat: TypeNat) : lcm: Nat ā Nat ā Natlcm m: Natm n: Natn = lcm: Nat ā Nat ā Natlcm n: Natn m: Natm := byGoals accomplished! š
m, n: Natlcm m n = lcm n mrw [m, n: Natlcm m n = lcm n mlcm: Nat ā Nat ā Natlcm,m, n: Natm * n / gcd m n = lcm n m m, n: Natlcm m n = lcm n mlcm: Nat ā Nat ā Natlcm,m, n: Natm * n / gcd m n = n * m / gcd n m m, n: Natlcm m n = lcm n mNat.mul_comm: ā (n m : Nat), n * m = m * nNat.mul_comm n: Natn m: Natm,m, n: Natm * n / gcd m n = m * n / gcd n m m, n: Natlcm m n = lcm n mgcd_comm: ā (m n : Nat), gcd m n = gcd n mgcd_comm n: Natn m: Natmm, n: Natm * n / gcd m n = m * n / gcd m n]Goals accomplished! š

@[simp] theorem lcm_zero_left: ā (m : Nat), lcm 0 m = 0lcm_zero_left (m: Natm : Nat: TypeNat) : lcm: Nat ā Nat ā Natlcm 0: ?m.55140 m: Natm = 0: ?m.55230 := byGoals accomplished! š m: Natlcm 0 m = 0simp [lcm: Nat ā Nat ā Natlcm]Goals accomplished! š

@[simp] theorem lcm_zero_right: ā (m : Nat), lcm m 0 = 0lcm_zero_right (m: Natm : Nat: TypeNat) : lcm: Nat ā Nat ā Natlcm m: Natm 0: ?m.56500 = 0: ?m.56590 := byGoals accomplished! š m: Natlcm m 0 = 0simp [lcm: Nat ā Nat ā Natlcm]Goals accomplished! š

@[simp] theorem lcm_one_left: ā (m : Nat), lcm 1 m = mlcm_one_left (m: Natm : Nat: TypeNat) : lcm: Nat ā Nat ā Natlcm 1: ?m.57821 m: Natm = m: Natm := byGoals accomplished! š m: Natlcm 1 m = msimp [lcm: Nat ā Nat ā Natlcm]Goals accomplished! š

@[simp] theorem lcm_one_right: ā (m : Nat), lcm m 1 = mlcm_one_right (m: Natm : Nat: TypeNat) : lcm: Nat ā Nat ā Natlcm m: Natm 1: ?m.59041 = m: Natm := byGoals accomplished! š m: Natlcm m 1 = msimp [lcm: Nat ā Nat ā Natlcm]Goals accomplished! š

@[simp] theorem lcm_self: ā (m : Nat), lcm m m = mlcm_self (m: Natm : Nat: TypeNat) : lcm: Nat ā Nat ā Natlcm m: Natm m: Natm = m: Natm := byGoals accomplished! š
m: Natlcm m m = mmatch eq_zero_or_pos: ā (n : Nat), n = 0 āØ n > 0eq_zero_or_pos m: Natm with
m: Natlcm m m = m| .inl: ā {a b : Prop}, a ā a āØ b.inl h: m = 0h =>m: Nath: m = 0lcm m m = m m: Natlcm m m = mrw [m: Nath: m = 0lcm m m = mh: m = 0h,m: Nath: m = 0lcm 0 0 = 0 m: Nath: m = 0lcm m m = mlcm_zero_left: ā (m : Nat), lcm 0 m = 0lcm_zero_leftm: Nath: m = 00 = 0]Goals accomplished! š
m: Natlcm m m = m| .inr: ā {a b : Prop}, b ā a āØ b.inr h: m > 0h =>m: Nath: m > 0lcm m m = m m: Natlcm m m = msimp [lcm: Nat ā Nat ā Natlcm, Nat.mul_div_cancel: ā (m : Nat) {n : Nat}, 0 < n ā m * n / n = mNat.mul_div_cancel _: Nat_ h: m > 0h]Goals accomplished! š

theorem dvd_lcm_left: ā (m n : Nat), m ā£ lcm m ndvd_lcm_left (m: Natm n: Natn : Nat: TypeNat) : m: Natm ā£ lcm: Nat ā Nat ā Natlcm m: Natm n: Natn :=
āØn: Natn / gcd: Nat ā Nat ā Natgcd m: Natm n: Natn, byGoals accomplished! š m, n: Natlcm m n = m * (n / gcd m n)rw [m, n: Natlcm m n = m * (n / gcd m n)ā Nat.mul_div_assoc: ā {k n : Nat} (m : Nat), k ā£ n ā m * n / k = m * (n / k)Nat.mul_div_assoc m: Natm (Nat.gcd_dvd_right: ā (m n : Nat), gcd m n ā£ nNat.gcd_dvd_right m: Natm n: Natn)m, n: Natlcm m n = m * n / gcd m n]m, n: Natlcm m n = m * n / gcd m n;m, n: Natlcm m n = m * n / gcd m n m, n: Natlcm m n = m * (n / gcd m n)rflGoals accomplished! šā©

theorem dvd_lcm_right: ā (m n : Nat), n ā£ lcm m ndvd_lcm_right (m: Natm n: Natn : Nat: TypeNat) : n: Natn ā£ lcm: Nat ā Nat ā Natlcm m: Natm n: Natn := lcm_comm: ā (m n : Nat), lcm m n = lcm n mlcm_comm n: Natn m: Natm āø dvd_lcm_left: ā (m n : Nat), m ā£ lcm m ndvd_lcm_left n: Natn m: Natm

theorem gcd_mul_lcm: ā (m n : Nat), gcd m n * lcm m n = m * ngcd_mul_lcm (m: Natm n: Natn : Nat: TypeNat) : gcd: Nat ā Nat ā Natgcd m: Natm n: Natn * lcm: Nat ā Nat ā Natlcm m: Natm n: Natn = m: Natm * n: Natn := byGoals accomplished! š
m, n: Natgcd m n * lcm m n = m * nrw [m, n: Natgcd m n * lcm m n = m * nlcm: Nat ā Nat ā Natlcm,m, n: Natgcd m n * (m * n / gcd m n) = m * n m, n: Natgcd m n * lcm m n = m * nNat.mul_div_cancel': ā {n m : Nat}, n ā£ m ā n * (m / n) = mNat.mul_div_cancel' (Nat.dvd_trans: ā {a b c : Nat}, a ā£ b ā b ā£ c ā a ā£ cNat.dvd_trans (gcd_dvd_left: ā (m n : Nat), gcd m n ā£ mgcd_dvd_left m: Natm n: Natn) (Nat.dvd_mul_right: ā (a b : Nat), a ā£ a * bNat.dvd_mul_right m: Natm n: Natn))m, n: Natm * n = m * n]Goals accomplished! š

theorem lcm_dvd: ā {m n k : Nat}, m ā£ k ā n ā£ k ā lcm m n ā£ klcm_dvd {m: Natm n: Natn k: Natk : Nat: TypeNat} (H1: m ā£ kH1 : m: Natm ā£ k: Natk) (H2: n ā£ kH2 : n: Natn ā£ k: Natk) : lcm: Nat ā Nat ā Natlcm m: Natm n: Natn ā£ k: Natk := byGoals accomplished! š
m, n, k: NatH1: m ā£ kH2: n ā£ klcm m n ā£ kmatch eq_zero_or_pos: ā (n : Nat), n = 0 āØ n > 0eq_zero_or_pos k: Natk with
m, n, k: NatH1: m ā£ kH2: n ā£ klcm m n ā£ k| .inl: ā {a b : Prop}, a ā a āØ b.inl h: k = 0h =>m, n, k: NatH1: m ā£ kH2: n ā£ kh: k = 0lcm m n ā£ k m, n, k: NatH1: m ā£ kH2: n ā£ klcm m n ā£ krw [m, n, k: NatH1: m ā£ kH2: n ā£ kh: k = 0lcm m n ā£ kh: k = 0hm, n, k: NatH1: m ā£ kH2: n ā£ kh: k = 0lcm m n ā£ 0]m, n, k: NatH1: m ā£ kH2: n ā£ kh: k = 0lcm m n ā£ 0;m, n, k: NatH1: m ā£ kH2: n ā£ kh: k = 0lcm m n ā£ 0 m, n, k: NatH1: m ā£ kH2: n ā£ kh: k = 0lcm m n ā£ kexact Nat.dvd_zero: ā (a : Nat), a ā£ 0Nat.dvd_zero _: Nat_Goals accomplished! š
m, n, k: NatH1: m ā£ kH2: n ā£ klcm m n ā£ k| .inr: ā {a b : Prop}, b ā a āØ b.inr kpos: k > 0kpos =>m, n, k: NatH1: m ā£ kH2: n ā£ kkpos: k > 0lcm m n ā£ k
m, n, k: NatH1: m ā£ kH2: n ā£ klcm m n ā£ kapply Nat.dvd_of_mul_dvd_mul_left: ā {k m n : Nat}, 0 < k ā k * m ā£ k * n ā m ā£ nNat.dvd_of_mul_dvd_mul_left (gcd_pos_of_pos_left: ā {m : Nat} (n : Nat), 0 < m ā 0 < gcd m ngcd_pos_of_pos_left n: Natn (pos_of_dvd_of_pos: ā {m n : Nat}, m ā£ n ā 0 < n ā 0 < mpos_of_dvd_of_pos H1: m ā£ kH1 kpos: k > 0kpos))m, n, k: NatH1: m ā£ kH2: n ā£ kkpos: k > 0gcd m n * lcm m n ā£ gcd m n * k
m, n, k: NatH1: m ā£ kH2: n ā£ kkpos: k > 0lcm m n ā£ krw [m, n, k: NatH1: m ā£ kH2: n ā£ kkpos: k > 0gcd m n * lcm m n ā£ gcd m n * kgcd_mul_lcm: ā (m n : Nat), gcd m n * lcm m n = m * ngcd_mul_lcm,m, n, k: NatH1: m ā£ kH2: n ā£ kkpos: k > 0m * n ā£ gcd m n * k m, n, k: NatH1: m ā£ kH2: n ā£ kkpos: k > 0gcd m n * lcm m n ā£ gcd m n * kā gcd_mul_right: ā (m n k : Nat), gcd (m * n) (k * n) = gcd m k * ngcd_mul_right,m, n, k: NatH1: m ā£ kH2: n ā£ kkpos: k > 0m * n ā£ gcd (m * k) (n * k) m, n, k: NatH1: m ā£ kH2: n ā£ kkpos: k > 0gcd m n * lcm m n ā£ gcd m n * kNat.mul_comm: ā (n m : Nat), n * m = m * nNat.mul_comm n: Natn k: Natkm, n, k: NatH1: m ā£ kH2: n ā£ kkpos: k > 0m * n ā£ gcd (m * k) (k * n)]m, n, k: NatH1: m ā£ kH2: n ā£ kkpos: k > 0m * n ā£ gcd (m * k) (k * n)
m, n, k: NatH1: m ā£ kH2: n ā£ kkpos: k > 0lcm m n ā£ kexact dvd_gcd: ā {k m n : Nat}, k ā£ m ā k ā£ n ā k ā£ gcd m ndvd_gcd (Nat.mul_dvd_mul_left: ā {b c : Nat} (a : Nat), b ā£ c ā a * b ā£ a * cNat.mul_dvd_mul_left _: Nat_ H2: n ā£ kH2) (Nat.mul_dvd_mul_right: ā {a b : Nat}, a ā£ b ā ā (c : Nat), a * c ā£ b * cNat.mul_dvd_mul_right H1: m ā£ kH1 _: Nat_)Goals accomplished! š

theorem lcm_assoc: ā (m n k : Nat), lcm (lcm m n) k = lcm m (lcm n k)lcm_assoc (m: Natm n: Natn k: Natk : Nat: TypeNat) : lcm: Nat ā Nat ā Natlcm (lcm: Nat ā Nat ā Natlcm m: Natm n: Natn) k: Natk = lcm: Nat ā Nat ā Natlcm m: Natm (lcm: Nat ā Nat ā Natlcm n: Natn k: Natk) :=
dvd_antisymm: ā {m n : Nat}, m ā£ n ā n ā£ m ā m = ndvd_antisymm
(lcm_dvd: ā {m n k : Nat}, m ā£ k ā n ā£ k ā lcm m n ā£ klcm_dvd
(lcm_dvd: ā {m n k : Nat}, m ā£ k ā n ā£ k ā lcm m n ā£ klcm_dvd (dvd_lcm_left: ā (m n : Nat), m ā£ lcm m ndvd_lcm_left m: Natm (lcm: Nat ā Nat ā Natlcm n: Natn k: Natk)) (Nat.dvd_trans: ā {a b c : Nat}, a ā£ b ā b ā£ c ā a ā£ cNat.dvd_trans (dvd_lcm_left: ā (m n : Nat), m ā£ lcm m ndvd_lcm_left n: Natn k: Natk) (dvd_lcm_right: ā (m n : Nat), n ā£ lcm m ndvd_lcm_right m: Natm (lcm: Nat ā Nat ā Natlcm n: Natn k: Natk))))
(Nat.dvd_trans: ā {a b c : Nat}, a ā£ b ā b ā£ c ā a ā£ cNat.dvd_trans (dvd_lcm_right: ā (m n : Nat), n ā£ lcm m ndvd_lcm_right n: Natn k: Natk) (dvd_lcm_right: ā (m n : Nat), n ā£ lcm m ndvd_lcm_right m: Natm (lcm: Nat ā Nat ā Natlcm n: Natn k: Natk))))
(lcm_dvd: ā {m n k : Nat}, m ā£ k ā n ā£ k ā lcm m n ā£ klcm_dvd
(Nat.dvd_trans: ā {a b c : Nat}, a ā£ b ā b ā£ c ā a ā£ cNat.dvd_trans (dvd_lcm_left: ā (m n : Nat), m ā£ lcm m ndvd_lcm_left m: Natm n: Natn) (dvd_lcm_left: ā (m n : Nat), m ā£ lcm m ndvd_lcm_left (lcm: Nat ā Nat ā Natlcm m: Natm n: Natn) k: Natk))
(lcm_dvd: ā {m n k : Nat}, m ā£ k ā n ā£ k ā lcm m n ā£ klcm_dvd (Nat.dvd_trans: ā {a b c : Nat}, a ā£ b ā b ā£ c ā a ā£ cNat.dvd_trans (dvd_lcm_right: ā (m n : Nat), n ā£ lcm m ndvd_lcm_right m: Natm n: Natn) (dvd_lcm_left: ā (m n : Nat), m ā£ lcm m ndvd_lcm_left (lcm: Nat ā Nat ā Natlcm m: Natm n: Natn) k: Natk))
(dvd_lcm_right: ā (m n : Nat), n ā£ lcm m ndvd_lcm_right (lcm: Nat ā Nat ā Natlcm m: Natm n: Natn) k: Natk)))

theorem lcm_ne_zero: ā {m n : Nat}, m ā  0 ā n ā  0 ā lcm m n ā  0lcm_ne_zero (hm: m ā  0hm : m: ?m.6758m ā  0: ?m.67840) (hn: n ā  0hn : n: ?m.6778n ā  0: ?m.67980) : lcm: Nat ā Nat ā Natlcm m: ?m.6758m n: ?m.6778n ā  0: ?m.68120 := byGoals accomplished! š
m, n: Nathm: m ā  0hn: n ā  0lcm m n ā  0intro h: lcm m n = 0hm, n: Nathm: m ā  0hn: n ā  0h: lcm m n = 0False
m, n: Nathm: m ā  0hn: n ā  0lcm m n ā  0have h1: ?m.6835h1 := gcd_mul_lcm: ā (m n : Nat), gcd m n * lcm m n = m * ngcd_mul_lcm m: Natm n: Natnm, n: Nathm: m ā  0hn: n ā  0h: lcm m n = 0h1: gcd m n * lcm m n = m * nFalse
m, n: Nathm: m ā  0hn: n ā  0lcm m n ā  0rw [m, n: Nathm: m ā  0hn: n ā  0h: lcm m n = 0h1: gcd m n * lcm m n = m * nFalseh: lcm m n = 0h,m, n: Nathm: m ā  0hn: n ā  0h: lcm m n = 0h1: gcd m n * 0 = m * nFalse m, n: Nathm: m ā  0hn: n ā  0h: lcm m n = 0h1: gcd m n * lcm m n = m * nFalseNat.mul_zero: ā (n : Nat), n * 0 = 0Nat.mul_zerom, n: Nathm: m ā  0hn: n ā  0h: lcm m n = 0h1: 0 = m * nFalse]m, n: Nathm: m ā  0hn: n ā  0h: lcm m n = 0h1: 0 = m * nFalse at h1: gcd m n * 0 = m * nh1m, n: Nathm: m ā  0hn: n ā  0h: lcm m n = 0h1: 0 = m * nFalse
m, n: Nathm: m ā  0hn: n ā  0lcm m n ā  0match mul_eq_zero: ā {n m : Nat}, n * m = 0 ā n = 0 āØ m = 0mul_eq_zero.1: ā {a b : Prop}, (a ā b) ā a ā b1 h1: 0 = m * nh1.symm: ā {Ī± : Sort ?u.6884} {a b : Ī±}, a = b ā b = asymm with
m, n: Nathm: m ā  0hn: n ā  0h: lcm m n = 0h1: 0 = m * nFalse| .inl: ā {a b : Prop}, a ā a āØ b.inl hm1: m = 0hm1 =>m, n: Nathm: m ā  0hn: n ā  0h: lcm m n = 0h1: 0 = m * nhm1: m = 0False m, n: Nathm: m ā  0hn: n ā  0h: lcm m n = 0h1: 0 = m * nFalseexact hm: m ā  0hm hm1: m = 0hm1Goals accomplished! š
m, n: Nathm: m ā  0hn: n ā  0h: lcm m n = 0h1: 0 = m * nFalse| .inr: ā {a b : Prop}, b ā a āØ b.inr hn1: n = 0hn1 =>m, n: Nathm: m ā  0hn: n ā  0h: lcm m n = 0h1: 0 = m * nhn1: n = 0False m, n: Nathm: m ā  0hn: n ā  0h: lcm m n = 0h1: 0 = m * nFalseexact hn: n ā  0hn hn1: n = 0hn1Goals accomplished! š

/-!
### `coprime`

-/

instance: (m n : Nat) ā Decidable (coprime m n)instance (m: Natm n: Natn : Nat: TypeNat) : Decidable: Prop ā TypeDecidable (coprime: Nat ā Nat ā Propcoprime m: Natm n: Natn) := inferInstanceAs: (Ī± : Sort ?u.7015) ā [i : Ī±] ā Ī±inferInstanceAs (Decidable: Prop ā TypeDecidable (_: ?m.7018_ = 1: ?m.70211))

theorem coprime_iff_gcd_eq_one: ā {m n : Nat}, coprime m n ā gcd m n = 1coprime_iff_gcd_eq_one : coprime: Nat ā Nat ā Propcoprime m: ?m.7130m n: ?m.7134n ā gcd: Nat ā Nat ā Natgcd m: ?m.7130m n: ?m.7134n = 1: ?m.71391 := .rfl: ā {a : Prop}, a ā a.rfl

theorem coprime.gcd_eq_one: ā {m n : Nat}, coprime m n ā gcd m n = 1coprime.gcd_eq_one : coprime: Nat ā Nat ā Propcoprime m: ?m.7168m n: ?m.7173n ā gcd: Nat ā Nat ā Natgcd m: ?m.7168m n: ?m.7173n = 1: ?m.71801 := id: ā {Ī± : Sort ?u.7201}, Ī± ā Ī±id

theorem coprime.symm: ā {n m : Nat}, coprime n m ā coprime m ncoprime.symm : coprime: Nat ā Nat ā Propcoprime n: ?m.7211n m: ?m.7216m ā coprime: Nat ā Nat ā Propcoprime m: ?m.7216m n: ?m.7211n := (gcd_comm: ā (m n : Nat), gcd m n = gcd n mgcd_comm m: Natm n: Natn).trans: ā {Ī± : Sort ?u.7227} {a b c : Ī±}, a = b ā b = c ā a = ctrans

theorem coprime_comm: ā {n m : Nat}, coprime n m ā coprime m ncoprime_comm : coprime: Nat ā Nat ā Propcoprime n: ?m.7248n m: ?m.7252m ā coprime: Nat ā Nat ā Propcoprime m: ?m.7252m n: ?m.7248n := āØcoprime.symm: ā {n m : Nat}, coprime n m ā coprime m ncoprime.symm, coprime.symm: ā {n m : Nat}, coprime n m ā coprime m ncoprime.symmā©

theorem coprime.dvd_of_dvd_mul_right: ā {k n m : Nat}, coprime k n ā k ā£ m * n ā k ā£ mcoprime.dvd_of_dvd_mul_right (H1: coprime k nH1 : coprime: Nat ā Nat ā Propcoprime k: ?m.7282k n: ?m.7286n) (H2: k ā£ m * nH2 : k: ?m.7282k ā£ m: ?m.7300m * n: ?m.7286n) : k: ?m.7282k ā£ m: ?m.7300m := byGoals accomplished! š
k, n, m: NatH1: coprime k nH2: k ā£ m * nk ā£ mlet t: ?m.7367t := dvd_gcd: ā {k m n : Nat}, k ā£ m ā k ā£ n ā k ā£ gcd m ndvd_gcd (Nat.dvd_mul_left: ā (a b : Nat), a ā£ b * aNat.dvd_mul_left k: Natk m: Natm) H2: k ā£ m * nH2k, n, m: NatH1: coprime k nH2: k ā£ m * nt:= dvd_gcd (Nat.dvd_mul_left k m) H2: k ā£ gcd (m * k) (m * n)k ā£ m
k, n, m: NatH1: coprime k nH2: k ā£ m * nk ā£ mrwa [k, n, m: NatH1: coprime k nH2: k ā£ m * nt:= dvd_gcd (Nat.dvd_mul_left k m) H2: k ā£ gcd (m * k) (m * n)k ā£ mgcd_mul_left: ā (m n k : Nat), gcd (m * n) (m * k) = m * gcd n kgcd_mul_left,k, n, m: NatH1: coprime k nH2: k ā£ m * nt: k ā£ m * gcd k nk ā£ m k, n, m: NatH1: coprime k nH2: k ā£ m * nt:= dvd_gcd (Nat.dvd_mul_left k m) H2: k ā£ gcd (m * k) (m * n)k ā£ mH1: coprime k nH1.gcd_eq_one: ā {m n : Nat}, coprime m n ā gcd m n = 1gcd_eq_one,k, n, m: NatH1: coprime k nH2: k ā£ m * nt: k ā£ m * 1k ā£ m k, n, m: NatH1: coprime k nH2: ```