proposition: Lemma Pos_iter_op_ok_0 : forall p x acc, is_power_of x acc -> pos_iter_M x acc p = binary_power_mult x acc p .
proof: Proof. induction p. - simpl. intros; rewrite IHp. rewrite (IHp x acc). repeat rewrite (binary_power_mult_ok M). rewrite <- (sqr_eqn M x). rewrite power_of_power. rewrite (Nat.mul_comm (Pos.to_nat p) 2)%nat. destruct H as [i e]. repeat rewrite (op_assoc (Monoid:=M)). subst acc. rewrite <- (power_commute_with_x ). replace (2* Pos.to_nat p)%nat with (Pos.to_nat p + Pos.to_nat p)%nat. + rewrite power_of_plus. now rewrite (op_assoc (Monoid:=M)). + ring. + assumption. + rewrite IHp;auto. rewrite (binary_power_mult_ok M). destruct H as [i Hi]. exists (i + Pos.to_nat p)%nat. rewrite power_of_plus. subst acc;auto. - simpl; intros; rewrite IHp. rewrite (IHp x acc). repeat rewrite (binary_power_mult_ok M); rewrite <- (sqr_eqn M). repeat (rewrite (op_assoc (Monoid:=M))). rewrite power_of_power. rewrite (Nat.mul_comm (Pos.to_nat p) 2)%nat. replace (2* Pos.to_nat p)%nat with (Pos.to_nat p + Pos.to_nat p)%nat. + rewrite power_of_plus;now rewrite op_assoc. + ring. + assumption. + rewrite IHp, (binary_power_mult_ok M). destruct H as [i Hi]. exists (i + Pos.to_nat p)%nat. rewrite power_of_plus. subst acc;auto. auto. - intros; simpl. change (op x acc) with (x * acc). destruct H as [i Hi]; subst acc. apply power_commute_with_x. Qed.
imports: additions(Monoid_def Monoid_instances Pow) Coq(Lia ArithRing)