proposition: Lemma Pos_iter_ok: forall p x, N_bpow x (Npos p) = pos_iter_M x one p.
proof: Proof. intros p x; rewrite Pos_iter_op_ok_0. unfold N_bpow. rewrite Pos_bpow_ok. generalize (binary_power_mult_ok M (E_eq := eq_equiv)). unfold equiv, eq_equiv. intro H; rewrite H. now rewrite (one_left (Monoid := M)). exists 0%nat. reflexivity. Qed.
imports: additions(Monoid_def Monoid_instances Pow) Coq(Lia ArithRing)