proposition: Lemma pow_pos_swap x j : pow_pos x j * x == x * pow_pos x j.
proof: Proof. induction j as [j IHj|j IHj|]; simpl; rewrite <- ?mul_assoc. - f_equiv. now do 2 (rewrite IHj, mul_assoc). - now do 2 (rewrite IHj, mul_assoc). - reflexivity. Qed.
imports: Setoid Morphisms BinPos BinNat