proposition: Lemma Pos_iter_op_ok: forall p x, pos_iter_M x one p = binary_power_mult x one p .
proof: Proof. intros p x; rewrite Pos_iter_op_ok_0;auto. now exists 0%nat. Qed.
imports: additions(Monoid_def Monoid_instances Pow) Coq(Lia ArithRing)