n : ℕ+
h : n < 2
⊢ n = 1
n : ℕ+
⊢ n < 2 → n = 1
intro h
case a
n : ℕ+
h : n < 2
⊢ n ≤ 1

case a
n : ℕ+
h : n < 2
⊢ 1 ≤ n
n : ℕ+
h : n < 2
⊢ n = 1
apply le_antisymm
case a
n : ℕ+
h : n < 2
⊢ 1 ≤ n

case a
n : ℕ+
h : n < 2
⊢ n ≤ 1
case a
n : ℕ+
h : n < 2
⊢ n ≤ 1

case a
n : ℕ+
h : n < 2
⊢ 1 ≤ n
swap
case a
n : ℕ+
h : n < 2
⊢ n ≤ 1
case a
n : ℕ+
h : n < 2
⊢ 1 ≤ n

case a
n : ℕ+
h : n < 2
⊢ n ≤ 1
apply PNat.one_le
no goals
case a
n : ℕ+
h : n < 2
⊢ n ≤ 1
exact PNat.lt_add_one_iff.1 h