proposition: Theorem Pmult_nat_plus_carry_morphism : forall p q n, Pmult_nat (Pos.add_carry p q) n = n + Pmult_nat (p + q) n.
proof: Proof. intros. now rewrite Pos.add_carry_spec, Pmult_nat_succ_morphism. Qed.
imports: BinPos PeanoNat