theorem Nat.ToInt.ofNat_toNat (a : Int) : ↑a.toNat = if a ≤ 0 then 0 else a

theorem Nat.ToInt.toNat_nonneg (x : Nat) : -1 * ↑x ≤ 0

theorem Nat.ToInt.natCast_ofNat (n : Nat) : ↑(OfNat.ofNat n) = OfNat.ofNat n

theorem Nat.ToInt.of_eq {a b : Nat} {a' b' : Int} (h₁ : ↑a = a') (h₂ : ↑b = b') : a = b → a' = b'

theorem Nat.ToInt.of_diseq {a b : Nat} {a' b' : Int} (h₁ : ↑a = a') (h₂ : ↑b = b') : a ≠ b → a' ≠ b'

theorem Nat.ToInt.of_dvd (d a : Nat) (d' a' : Int) (h₁ : ↑d = d') (h₂ : ↑a = a') : d ∣ a → d' ∣ a'

theorem Nat.ToInt.of_le {a b : Nat} {a' b' : Int} (h₁ : ↑a = a') (h₂ : ↑b = b') : a ≤ b → a' ≤ b'

theorem Nat.ToInt.of_not_le {a b : Nat} {a' b' : Int} (h₁ : ↑a = a') (h₂ : ↑b = b') : ¬a ≤ b → b' + 1 ≤ a'

theorem Nat.ToInt.add_congr {a b : Nat} {a' b' : Int} (h₁ : ↑a = a') (h₂ : ↑b = b') : ↑(a + b) = a' + b'

theorem Nat.ToInt.mul_congr {a b : Nat} {a' b' : Int} (h₁ : ↑a = a') (h₂ : ↑b = b') : ↑(a * b) = a' * b'

theorem Nat.ToInt.sub_congr {a b : Nat} {a' b' : Int} (h₁ : ↑a = a') (h₂ : ↑b = b') : ↑(a - b) = if b' + -1 * a' ≤ 0 then a' - b' else 0

theorem Nat.ToInt.pow_congr {a : Nat} (k : Nat) (a' : Int) (h₁ : ↑a = a') : ↑(a ^ k) = a' ^ k

theorem Nat.ToInt.div_congr {a b : Nat} {a' b' : Int} (h₁ : ↑a = a') (h₂ : ↑b = b') : ↑(a / b) = a' / b'

theorem Nat.ToInt.mod_congr {a b : Nat} {a' b' : Int} (h₁ : ↑a = a') (h₂ : ↑b = b') : ↑(a % b) = a' % b'

theorem Nat.ToInt.finVal {n : Nat} {a : Fin n} {a' : Int} (h₁ : ↑a = a') : ↑↑a = a'

theorem Nat.ToInt.eq_eq {a b : Nat} {a' b' : Int} (h₁ : ↑a = a') (h₂ : ↑b = b') : (a = b) = (a' = b')

theorem Nat.ToInt.lt_eq {a b : Nat} {a' b' : Int} (h₁ : ↑a = a') (h₂ : ↑b = b') : (a < b) = (a' < b')

theorem Nat.ToInt.le_eq {a b : Nat} {a' b' : Int} (h₁ : ↑a = a') (h₂ : ↑b = b') : (a ≤ b) = (a' ≤ b')

def Int.Nonneg.num_cert (a : Int) : Bool

Equations

• Int.Nonneg.num_cert a = decide (a ≥ 0)

theorem Int.Nonneg.num (a : Int) : num_cert a = true → a ≥ 0

theorem Int.Nonneg.add (a b : Int) (h₁ : a ≥ 0) (h₂ : b ≥ 0) : a + b ≥ 0

theorem Int.Nonneg.mul (a b : Int) (h₁ : a ≥ 0) (h₂ : b ≥ 0) : a * b ≥ 0

theorem Int.Nonneg.div (a b : Int) (h₁ : a ≥ 0) (h₂ : b ≥ 0) : a / b ≥ 0

theorem Int.Nonneg.pow (a : Int) (k : Nat) (h₁ : a ≥ 0) : a ^ k ≥ 0

theorem Int.Nonneg.mod (a b : Int) (h₁ : a ≥ 0) : a % b ≥ 0

theorem Int.Nonneg.natCast (a : Nat) : ↑a ≥ 0

theorem Int.Nonneg.toPoly (e : Int) : e ≥ 0 → -1 * e ≤ 0