proposition: Lemma pow_pos_add x i j : pow_pos x (i + j) == pow_pos x i * pow_pos x j.
proof: Proof. induction i as [|i IHi] using Pos.peano_ind. - now rewrite Pos.add_1_l, pow_pos_succ. - now rewrite Pos.add_succ_l, !pow_pos_succ, IHi, mul_assoc. Qed.
imports: Setoid Morphisms BinPos BinNat