source
theorem Nat.ToInt.ofNat_toNat (a : Int) :
↑a.toNat = if a ≤ 0 then 0 else a
source
theorem Nat.ToInt.toNat_nonneg (x : Nat) :
-1 * ↑x ≤ 0
source
theorem Nat.ToInt.natCast_ofNat (n : Nat) :
↑(OfNat.ofNat n) = OfNat.ofNat n
source
theorem Nat.ToInt.of_eq {a b : Nat} {a' b' : Int} (h₁ : ↑a = a') (h₂ : ↑b = b') :
a = b → a' = b'
source
theorem Nat.ToInt.of_diseq {a b : Nat} {a' b' : Int} (h₁ : ↑a = a') (h₂ : ↑b = b') :
a ≠ b → a' ≠ b'
source
theorem Nat.ToInt.of_dvd (d a : Nat) (d' a' : Int) (h₁ : ↑d = d') (h₂ : ↑a = a') :
d ∣ a → d' ∣ a'
source
theorem Nat.ToInt.of_le {a b : Nat} {a' b' : Int} (h₁ : ↑a = a') (h₂ : ↑b = b') :
a ≤ b → a' ≤ b'
source
theorem Nat.ToInt.of_not_le {a b : Nat} {a' b' : Int} (h₁ : ↑a = a') (h₂ : ↑b = b') :
¬a ≤ b → b' + 1 ≤ a'
source
theorem Nat.ToInt.add_congr {a b : Nat} {a' b' : Int} (h₁ : ↑a = a') (h₂ : ↑b = b') :
↑(a + b) = a' + b'
source
theorem Nat.ToInt.mul_congr {a b : Nat} {a' b' : Int} (h₁ : ↑a = a') (h₂ : ↑b = b') :
↑(a * b) = a' * b'
source
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
source
theorem Nat.ToInt.pow_congr {a : Nat} (k : Nat) (a' : Int) (h₁ : ↑a = a') :
↑(a ^ k) = a' ^ k
source
theorem Nat.ToInt.div_congr {a b : Nat} {a' b' : Int} (h₁ : ↑a = a') (h₂ : ↑b = b') :
↑(a / b) = a' / b'
source
theorem Nat.ToInt.mod_congr {a b : Nat} {a' b' : Int} (h₁ : ↑a = a') (h₂ : ↑b = b') :
↑(a % b) = a' % b'
source
theorem Nat.ToInt.finVal {n : Nat} {a : Fin n} {a' : Int} (h₁ : ↑a = a') :
↑↑a = a'
source
theorem Nat.ToInt.eq_eq {a b : Nat} {a' b' : Int} (h₁ : ↑a = a') (h₂ : ↑b = b') :
(a = b) = (a' = b')
source
theorem Nat.ToInt.lt_eq {a b : Nat} {a' b' : Int} (h₁ : ↑a = a') (h₂ : ↑b = b') :
(a < b) = (a' < b')
source
theorem Nat.ToInt.le_eq {a b : Nat} {a' b' : Int} (h₁ : ↑a = a') (h₂ : ↑b = b') :
(a ≤ b) = (a' ≤ b')
source
def Int.Nonneg.num_cert (a : Int) :
Bool
Equations

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

Instances For

source
theorem Int.Nonneg.num (a : Int) :
num_cert a = true → a ≥ 0
source
theorem Int.Nonneg.add (a b : Int) (h₁ : a ≥ 0) (h₂ : b ≥ 0) :
a + b ≥ 0
source
theorem Int.Nonneg.mul (a b : Int) (h₁ : a ≥ 0) (h₂ : b ≥ 0) :
a * b ≥ 0
source
theorem Int.Nonneg.div (a b : Int) (h₁ : a ≥ 0) (h₂ : b ≥ 0) :
a / b ≥ 0
source
theorem Int.Nonneg.pow (a : Int) (k : Nat) (h₁ : a ≥ 0) :
a ^ k ≥ 0
source
theorem Int.Nonneg.mod (a b : Int) (h₁ : a ≥ 0) :
a % b ≥ 0
source
theorem Int.Nonneg.natCast (a : Nat) :
↑a ≥ 0
source
theorem Int.Nonneg.toPoly (e : Int) :
e ≥ 0 → -1 * e ≤ 0