proposition: Lemma pow_pos_add : forall x i j, pow_pos x (i + j) == pow_pos x i * pow_pos x j.
proof: Proof. intro x;induction i;intros. - rewrite Pos.xI_succ_xO;rewrite <- Pos.add_1_r. rewrite <- Pos.add_diag;repeat rewrite <- Pos.add_assoc. repeat rewrite IHi. rewrite Pos.add_comm;rewrite Pos.add_1_r; rewrite pow_pos_succ. simpl;repeat rewrite ring_mul_assoc. reflexivity. - rewrite <- Pos.add_diag;repeat rewrite <- Pos.add_assoc. repeat rewrite IHi. rewrite ring_mul_assoc. reflexivity. - rewrite Pos.add_comm;rewrite Pos.add_1_r;rewrite pow_pos_succ. simpl. reflexivity. Qed.
imports: Setoid BinPos BinNat Morphisms Setoid Bool ZArith_base Algebra_syntax