proposition: Lemma inj_add (n m : nat) : n<>0 -> m<>0 -> Pos.of_nat (n+m) = (Pos.of_nat n + Pos.of_nat m)%positive.
proof: Proof. intros Hn Hm. apply Pos2Nat.inj. rewrite Pos2Nat.inj_add, !id; trivial. intros H. destruct n. - now destruct Hn. - now simpl in H. Qed.
imports: BinPos PeanoNat