proposition: Theorem inj_mul p q : to_nat (p * q) = to_nat p * to_nat q.
proof: Proof. revert q. induction p as [|p IHp] using peano_ind; simpl; intros; trivial. now rewrite mul_succ_l, inj_add, IHp, inj_succ. Qed.
imports: BinPos PeanoNat