proposition: Theorem inj_add p q : to_nat (p + q) = to_nat p + to_nat q.
proof: Proof. revert q. induction p as [|p IHp] using peano_ind; intros q. - now rewrite add_1_l, inj_succ. - now rewrite add_succ_l, !inj_succ, IHp. Qed.
imports: BinPos PeanoNat