inductive MyNat : Type

• zero : MyNat
• succ : MyNat → MyNat

def MyNat.toNat : MyNat → ℕ

Equations

• MyNat.zero.toNat = 0
• n.succ.toNat = n.toNat.succ

def MyNat.fromNat : ℕ → MyNat

Equations

• MyNat.fromNat Nat.zero = MyNat.zero
• MyNat.fromNat n.succ = (MyNat.fromNat n).succ

instance MyNat.instOfNat {n : ℕ} : OfNat MyNat n

Equations

• MyNat.instOfNat = { ofNat := MyNat.fromNat n }

instance MyNat.instRepr : Repr MyNat

Equations

• MyNat.instRepr = { reprPrec := fun (n : MyNat) (x : ℕ) => Std.Format.text (toString "" ++ toString n.toNat ++ toString "") }

def MyNat.repeatn (f : MyNat → MyNat) (n i : MyNat) : MyNat

Equations

• MyNat.repeatn f MyNat.zero i = i
• MyNat.repeatn f n'.succ i = f (MyNat.repeatn f n' i)

def MyNat.addn (n : MyNat) : MyNat → MyNat

Equations

• n.addn = MyNat.repeatn MyNat.succ n

def MyNat.add (n m : MyNat) : MyNat

Equations

• n.add m = n.addn m

def MyNat.mul (n m : MyNat) : MyNat

Equations

• n.mul m = MyNat.repeatn n.addn m 0

instance MyNat.instAdd : Add MyNat

Equations

• MyNat.instAdd = { add := MyNat.add }

instance MyNat.instMul : Mul MyNat

Equations

• MyNat.instMul = { mul := MyNat.mul }

@[simp]

theorem MyNat.add_zero (n : MyNat) : zero + n = n

@[simp]

theorem MyNat.zero_add (n : MyNat) : n + zero = n

@[simp]

theorem MyNat.add_succ (n m : MyNat) : n.succ + m = (n + m).succ

@[simp]

theorem MyNat.succ_add (n m : MyNat) : n + m.succ = (n + m).succ

@[simp]

theorem MyNat.add_comm (m n : MyNat) : m + n = n + m

@[simp]

theorem MyNat.add_assoc (l m n : MyNat) : l + m + n = l + (m + n)

theorem MyNat.add_elim {n m : MyNat} : n + m = n → m = zero

theorem MyNat.add_eq_zero (n m : MyNat) : n + m = zero → m = zero

theorem MyNat.add_abac {a b c : MyNat} : a + b = a + c ↔ b = c

@[simp]

theorem MyNat.mul_zero (n : MyNat) : zero * n = zero

@[simp]

theorem MyNat.zero_mul (n : MyNat) : n * zero = zero

theorem MyNat.mul_one (m : MyNat) : m * zero.succ = m

@[simp]

theorem MyNat.one_mul (m : MyNat) : zero.succ * m = m

@[simp]

theorem MyNat.mul_succ (m n : MyNat) : m * n.succ = m + m * n

@[simp]

theorem MyNat.succ_mul (m n : MyNat) : m.succ * n = n + m * n

theorem MyNat.mul_comm (n m : MyNat) : n * m = m * n

@[simp]

theorem MyNat.mul_dist (l m n : MyNat) : l * (m + n) = l * m + l * n

theorem MyNat.mul_assoc (l m n : MyNat) : l * m * n = l * (m * n)

instance MyNat.instNatCast : NatCast MyNat

Equations

• MyNat.instNatCast = { natCast := MyNat.fromNat }

def MyNat.nsmul : ℕ → MyNat → MyNat

Equations

• MyNat.nsmul a b = ↑a * b

instance MyNat.instHMulNat : HMul ℕ MyNat MyNat

Equations

• MyNat.instHMulNat = { hMul := MyNat.nsmul }

instance MyNat.instHPowNat : HPow MyNat ℕ MyNat

Equations

• MyNat.instHPowNat = { hPow := fun (a : MyNat) (b : ℕ) => MyNat.repeatn a.mul (MyNat.fromNat b) 1 }

instance MyNat.instCommSemiring : Lean.Grind.CommSemiring MyNat

Equations

• One or more equations did not get rendered due to their size.

instance MyNat.instCommSemiring_1 : CommSemiring MyNat

Equations

• One or more equations did not get rendered due to their size.

def MyNat.le (n m : MyNat) : Prop

Equations

• (n <= m) = ∃ (c : MyNat), n + c = m

def MyNat.«term_<=_» : Lean.TrailingParserDescr

Equations

• MyNat.«term_<=_» = Lean.ParserDescr.trailingNode `MyNat.«term_<=_» 50 51 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " <= ") (Lean.ParserDescr.cat `term 51))

theorem MyNat.le_refl (n : MyNat) : n <= n

theorem MyNat.le_step (n m : MyNat) : n <= m → n <= m.succ

theorem MyNat.le_trans (l m n : MyNat) : l <= m → m <= n → l <= n

theorem MyNat.le_asym (n m : MyNat) : n <= m → m <= n → n = m

theorem MyNat.le_total (n m : MyNat) : n <= m ∨ m <= n

def MyNat.lt (n m : MyNat) : Prop

Equations

• (n < m) = (n <= m ∧ ¬n = m)

def MyNat.«term_<_» : Lean.TrailingParserDescr

Equations

• MyNat.«term_<_» = Lean.ParserDescr.trailingNode `MyNat.«term_<_» 50 51 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " < ") (Lean.ParserDescr.cat `term 51))

theorem MyNat.not_eq_succ (m n : MyNat) : ¬m + n.succ = m

theorem MyNat.lt_le_succ (n m : MyNat) : n < m ↔ n.succ <= m

theorem MyNat.lt_trans (l m n : MyNat) : l < m → m < n → l < n

theorem MyNat.mul_elim (n m : MyNat) : zero < n → n * m = n → m = 1

theorem MyNat.mul_eq_one (n m : MyNat) : n * m = 1 → n = 1

def MyNat.divides (d n : MyNat) : Prop

Equations

• (d ∣ n) = ∃ (k : MyNat), d * k = n

def MyNat.«term_∣_» : Lean.TrailingParserDescr

Equations

• MyNat.«term_∣_» = Lean.ParserDescr.trailingNode `MyNat.«term_∣_» 50 51 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ∣ ") (Lean.ParserDescr.cat `term 51))

theorem MyNat.zero_divides_only_zero (n : MyNat) : zero ∣ n → n = 0

theorem MyNat.all_divides_zero (d : MyNat) : d ∣ zero

theorem MyNat.divides_trans (d n m : MyNat) : d ∣ n → n ∣ m → d ∣ m

theorem MyNat.divides_assym (n m : MyNat) : n ∣ m → m ∣ n → n = m

theorem MyNat.le1 {a b : MyNat} : a + b <= a → b = 0

theorem MyNat.mul_le {a b c : MyNat} : a.succ * b <= a.succ * c → b <= c

theorem MyNat.divides_elim {a b c d : MyNat} : a + b = c → d ∣ a → d ∣ c → d ∣ b

def MyNat.eq_dec (n m : MyNat) : Bool

Equations

• MyNat.zero.eq_dec MyNat.zero = true
• MyNat.zero.eq_dec n.succ = false
• n_1.succ.eq_dec MyNat.zero = false
• n_1.succ.eq_dec n.succ = n_1.eq_dec n

@[simp]

theorem MyNat.eq_dec1 (n m : MyNat) : n.eq_dec m = true ↔ n = m

instance MyNat.eq_dec2 (n m : MyNat) : Decidable (n = m)

Equations

• One or more equations did not get rendered due to their size.

def MyNat.mod (n m : MyNat) : MyNat

Equations

• MyNat.zero % m = MyNat.zero
• n_1.succ % m = match (n_1 % m).succ.eq_dec m with | true => MyNat.zero | false => (n_1 % m).succ

def MyNat.«term_%_» : Lean.TrailingParserDescr

Equations

• MyNat.«term_%_» = Lean.ParserDescr.trailingNode `MyNat.«term_%_» 100 101 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " % ") (Lean.ParserDescr.cat `term 101))

theorem MyNat.mod_eq (n m : MyNat) : ∃ (c : MyNat), c * m + n % m = n

theorem MyNat.mod_lt (n m : MyNat) : 0 < m → n % m < m

@[simp]

theorem MyNat.succ_nat_mynat (n : MyNat) : n.succ.toNat = n.toNat.succ

@[simp]

theorem MyNat.succ_mynat_nat (n : ℕ) : fromNat n.succ = (fromNat n).succ

@[simp]

theorem MyNat.add_mynat_nat (n m : ℕ) : fromNat (n + m) = fromNat n + fromNat m

@[simp]

theorem MyNat.add_nat_mynat (n m : MyNat) : (n + m).toNat = n.toNat + m.toNat

theorem MyNat.to_from_nat (n : MyNat) : fromNat n.toNat = n

theorem MyNat.add_tonat {n m : MyNat} : (n + m).toNat = n.toNat + m.toNat

theorem MyNat.lt_tonat {n m : MyNat} : n < m → n.toNat.lt m.toNat

@[irreducible]

def MyNat.gcd (n m : MyNat) : MyNat

Equations

• n.gcd MyNat.zero = n
• n.gcd a.succ = a.succ.gcd (n % a.succ)

theorem MyNat.ind_mynat1 (P : MyNat → Prop) : (∀ (n : MyNat), (∀ (k : MyNat), k < n → P k) → P n) → ∀ (n k : MyNat), k <= n → P k

theorem MyNat.zero_le (k : MyNat) : zero <= k

theorem MyNat.ind_mynat (P : MyNat → Prop) : (∀ (n : MyNat), (∀ (k : MyNat), k < n → P k) → P n) → ∀ (n : MyNat), P n

theorem MyNat.zero0 : zero = 0

theorem MyNat.succ_le (a : MyNat) : a < a.succ

theorem MyNat.zero_lt_succ (a : MyNat) : zero < a.succ

theorem MyNat.gcd_linear (b a : MyNat) : ∃ (p : MyNat) (q : MyNat) (r : MyNat) (s : MyNat), p * a + q * b = r * a + s * b + a.gcd b

theorem MyNat.gcd_greatest (b a d : MyNat) : d ∣ a → d ∣ b → d ∣ a.gcd b

theorem MyNat.mod_le {a b : MyNat} : a < b → a % b = a

theorem MyNat.mod_aa {a : MyNat} : a % a = zero

theorem MyNat.gcd_aa (a : MyNat) : a.gcd a = a

theorem MyNat.gcd_divides_a_and_b {a b : MyNat} : a.gcd b ∣ a ∧ a.gcd b ∣ b

theorem MyNat.gcd_unique {a b : MyNat} (g1 g2 : MyNat) : g1 ∣ a ∧ g2 ∣ a ∧ g1 ∣ b ∧ g2 ∣ b → (∀ (d : MyNat), d ∣ a ∧ d ∣ b → d ∣ g1) → (∀ (d : MyNat), d ∣ a ∧ d ∣ b → d ∣ g2) → g1 = g2

theorem MyNat.gcd_comm (a b : MyNat) : a.gcd b = b.gcd a

def MyNat.tacticAuto : Lean.ParserDescr

Equations

• MyNat.tacticAuto = Lean.ParserDescr.node `MyNat.tacticAuto 1024 (Lean.ParserDescr.nonReservedSymbol "auto" false)

theorem MyNat.gcd_assoc (a b c : MyNat) : a.gcd (b.gcd c) = (a.gcd b).gcd c

def MyNat.is_prime (p : MyNat) : Prop

Equations

• p.is_prime = (MyNat.zero.succ < p ∧ ∀ (k : MyNat), k ∣ p → k = MyNat.zero.succ ∨ k = p)

theorem MyNat.pabpapb (p a b : MyNat) : p.is_prime → p ∣ a * b → p ∣ a ∨ p ∣ b

theorem MyNat.mynat_acc (n : MyNat) : Acc lt n