n m : ℕ
h : n ≤ m
⊢ (!decide (n = 0)) ≤ !decide (m = 0)
n m : ℕ
h : n ≤ m
⊢ ofNat n ≤ ofNat m
simp only [ofNat, ne_eq, _root_.decide_not]
no goals
n m : ℕ
h : n ≤ m
⊢ (!decide (n = 0)) ≤ !decide (m = 0)
cases Nat.decEq n 0 with
| isTrue hn => rw [decide_eq_true hn]; exact false_le
| isFalse hn =>
  cases Nat.decEq m 0 with
  | isFalse hm => rw [decide_eq_false hm]; exact le_true
  | isTrue hm => subst hm; have h := le_antisymm h (Nat.zero_le n); contradiction
case isTrue
n m : ℕ
h : n ≤ m
hn : n = 0
⊢ (!true) ≤ !decide (m = 0)
case isTrue
n m : ℕ
h : n ≤ m
hn : n = 0
⊢ (!decide (n = 0)) ≤ !decide (m = 0)
rw [decide_eq_true hn]
no goals
case isTrue
n m : ℕ
h : n ≤ m
hn : n = 0
⊢ (!true) ≤ !decide (m = 0)
exact false_le
no goals
case isFalse
n m : ℕ
h : n ≤ m
hn : ¬n = 0
⊢ (!decide (n = 0)) ≤ !decide (m = 0)
cases Nat.decEq m 0 with
| isFalse hm => rw [decide_eq_false hm]; exact le_true
| isTrue hm => subst hm; have h := le_antisymm h (Nat.zero_le n); contradiction
case isFalse.isFalse
n m : ℕ
h : n ≤ m
hn : ¬n = 0
hm : ¬m = 0
⊢ (!decide (n = 0)) ≤ !false
case isFalse.isFalse
n m : ℕ
h : n ≤ m
hn : ¬n = 0
hm : ¬m = 0
⊢ (!decide (n = 0)) ≤ !decide (m = 0)
rw [decide_eq_false hm]
no goals
case isFalse.isFalse
n m : ℕ
h : n ≤ m
hn : ¬n = 0
hm : ¬m = 0
⊢ (!decide (n = 0)) ≤ !false
exact le_true
case isFalse.isTrue
n : ℕ
hn : ¬n = 0
h : n ≤ 0
⊢ (!decide (n = 0)) ≤ !decide (0 = 0)
case isFalse.isTrue
n m : ℕ
h : n ≤ m
hn : ¬n = 0
hm : m = 0
⊢ (!decide (n = 0)) ≤ !decide (m = 0)
subst hm
case isFalse.isTrue
n : ℕ
hn : ¬n = 0
h✝ : n ≤ 0
h : n = 0
⊢ (!decide (n = 0)) ≤ !decide (0 = 0)
case isFalse.isTrue
n : ℕ
hn : ¬n = 0
h : n ≤ 0
⊢ (!decide (n = 0)) ≤ !decide (0 = 0)
have h := le_antisymm h (Nat.zero_le n)
no goals
case isFalse.isTrue
n : ℕ
hn : ¬n = 0
h✝ : n ≤ 0
h : n = 0
⊢ (!decide (n = 0)) ≤ !decide (0 = 0)
contradiction