Use the induction "tactic" here
Minor cleanup of Nat.pi