proposition: Lemma PN (SR : semiRingType) : @power_theory SR 1 *%R eq N id (fun x n => x ^+ nat_of_N n).
proof: Proof. split => r [] //=; elim=> //= p <-. - by rewrite Pos2Nat.inj_xI ?exprS -exprD addnn -mul2n. - by rewrite Pos2Nat.inj_xO ?exprS -exprD addnn -mul2n. Qed.
imports: elpi(elpi) Coq(QArith) Coq.micromega(OrderedRing RingMicromega) mathcomp(all_ssreflect ssralg ssrnum ssrint) mathcomp.zify(ssrZ zify)