proposition: Lemma AM_power_Ok {A : Type} `(M: @EMonoid A E_op E_one E_eq) (x:A) (n:positive): result_equiv (AM_power M x n) (Some (Pos_bpow x n, nil)).
proof: Proof. intros;eapply L0. Qed.
imports: Coq(List PArith Relations Lia) additions(Monoid_def Monoid_instances Strategies) Coq(Recdef Wf_nat) additions(More_on_positive Pow Euclidean_Chains Dichotomy BinaryStrat) Coq(NArith)