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