proposition: Lemma Rpower : power_theory 1 *%R eq nat_of_N (@GRing.exp R).
proof: Proof. apply: mkpow_th => x n; case: n => [//|p]; elim: p => [p|p|//] /= IHp. - by rewrite Pos2Nat.inj_xI exprS multE mulnC exprM expr2 IHp. - by rewrite Pos2Nat.inj_xO multE mulnC exprM expr2 IHp. Qed.
imports: elpi(elpi) Coq(QArith) Coq.micromega(OrderedRing RingMicromega) mathcomp(all_ssreflect ssralg ssrnum ssrint) mathcomp.zify(ssrZ zify)