proposition: Lemma pow_pos_succ : forall x j, pow_pos x (Pos.succ j) == x * pow_pos x j.
proof: Proof. induction j; simpl. - rewrite IHj. rewrite <- (ring_mul_assoc x (pow_pos x j) (x * pow_pos x j)). rewrite (ring_mul_assoc (pow_pos x j) x (pow_pos x j)). rewrite <- pow_pos_comm. rewrite <- ring_mul_assoc. reflexivity. - reflexivity. - reflexivity. Qed.
imports: Setoid BinPos BinNat Morphisms Setoid Bool ZArith_base Algebra_syntax