a b : ℕ+
⊢ ↑(toPNat' (↑a - ↑b)) = if b < a then ↑a - ↑b else 1
a b : ℕ+
⊢ ↑(a - b) = if b < a then ↑a - ↑b else 1
change (toPNat' _ : ℕ) = ite _ _ _
case inl
a b : ℕ+
h : b < a
⊢ ↑(toPNat' (↑a - ↑b)) = ↑a - ↑b

case inr
a b : ℕ+
h : ¬b < a
⊢ ↑(toPNat' (↑a - ↑b)) = 1
a b : ℕ+
⊢ ↑(toPNat' (↑a - ↑b)) = if b < a then ↑a - ↑b else 1
split_ifs with h
no goals
case inl
a b : ℕ+
h : b < a
⊢ ↑(toPNat' (↑a - ↑b)) = ↑a - ↑b
exact toPNat'_coe (tsub_pos_of_lt h)
case inr
a b : ℕ+
h : ¬b < a
⊢ ↑(toPNat' 0) = 1
case inr
a b : ℕ+
h : ¬b < a
⊢ ↑(toPNat' (↑a - ↑b)) = 1
rw [tsub_eq_zero_iff_le.mpr (le_of_not_gt h : (a : ℕ) ≤ b)]
no goals
case inr
a b : ℕ+
h : ¬b < a
⊢ ↑(toPNat' 0) = 1
rfl