Theorem: Imo2009P5.pnat_to_nat_prop (Compfiles/Imo2009P5.lean)

State before:
P : ℕ+ → Prop
h : ∀ (n : ℕ), P n.succPNat
n : ℕ+
⊢ P n
Tactic:
rw [← PNat.succPNat_natPred n]
State after:
P : ℕ+ → Prop
h : ∀ (n : ℕ), P n.succPNat
n : ℕ+
⊢ P n.natPred.succPNat

State before:
P : ℕ+ → Prop
h : ∀ (n : ℕ), P n.succPNat
n : ℕ+
⊢ P n.natPred.succPNat
Tactic:
exact h _
State after:
no goals