Theorem: nat_not_0_not_1 (Pdl/MultisetOrder.lean)

State before:
⊢ ∀ (n : ℕ), n ≠ 0 → n ≠ 1 → n ≥ 2
Tactic:
intros n h0 h1
State after:
n : ℕ
h0 : n ≠ 0
h1 : n ≠ 1
⊢ n ≥ 2

State before:
n : ℕ
h0 : n ≠ 0
h1 : n ≠ 1
⊢ n ≥ 2
Tactic:
cases n
State after:
case zero
h0 : 0 ≠ 0
h1 : 0 ≠ 1
⊢ 0 ≥ 2

case succ
n✝ : ℕ
h0 : n✝ + 1 ≠ 0
h1 : n✝ + 1 ≠ 1
⊢ n✝ + 1 ≥ 2

State before:
h0 : 0 ≠ 0
h1 : 0 ≠ 1
⊢ 0 ≥ 2
Tactic:
case zero => contradiction
State after:
no goals

State before:
m : ℕ
h0 : m + 1 ≠ 0
h1 : m + 1 ≠ 1
⊢ m + 1 ≥ 2
Tactic:
case succ m =>
  cases m
  case zero => contradiction
  case succ n=>
    apply Nat.succ_le_succ
    aesop
State after:
no goals

State before:
h0 : 0 ≠ 0
h1 : 0 ≠ 1
⊢ 0 ≥ 2
Tactic:
contradiction
State after:
no goals

State before:
m : ℕ
h0 : m + 1 ≠ 0
h1 : m + 1 ≠ 1
⊢ m + 1 ≥ 2
Tactic:
cases m
State after:
case zero
h0 : 0 + 1 ≠ 0
h1 : 0 + 1 ≠ 1
⊢ 0 + 1 ≥ 2

case succ
n✝ : ℕ
h0 : n✝ + 1 + 1 ≠ 0
h1 : n✝ + 1 + 1 ≠ 1
⊢ n✝ + 1 + 1 ≥ 2

State before:
h0 : 0 + 1 ≠ 0
h1 : 0 + 1 ≠ 1
⊢ 0 + 1 ≥ 2
Tactic:
case zero => contradiction
State after:
no goals

State before:
n : ℕ
h0 : n + 1 + 1 ≠ 0
h1 : n + 1 + 1 ≠ 1
⊢ n + 1 + 1 ≥ 2
Tactic:
case succ n=>
  apply Nat.succ_le_succ
  aesop
State after:
no goals

State before:
h0 : 0 + 1 ≠ 0
h1 : 0 + 1 ≠ 1
⊢ 0 + 1 ≥ 2
Tactic:
contradiction
State after:
no goals

State before:
n : ℕ
h0 : n + 1 + 1 ≠ 0
h1 : n + 1 + 1 ≠ 1
⊢ n + 1 + 1 ≥ 2
Tactic:
apply Nat.succ_le_succ
State after:
case a
n : ℕ
h0 : n + 1 + 1 ≠ 0
h1 : n + 1 + 1 ≠ 1
⊢ 1 ≤ n + 1

State before:
case a
n : ℕ
h0 : n + 1 + 1 ≠ 0
h1 : n + 1 + 1 ≠ 1
⊢ 1 ≤ n + 1
Tactic:
aesop
State after:
no goals