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