proposition: Lemma RSORaddon : @SORaddon R 0 1 +%R *%R (fun x y => x - y) -%R eq (fun x y => x <= y) Z Z0 (Zpos 1) Z.add Z.mul Z.sub Z.opp Z.eqb Z.leb (fun n => (int_of_Z n)%:~R) nat nat_of_N (@GRing.exp R).
proof: Proof. apply: mk_SOR_addon. - exact: RZ. - exact: Rpower. - by move=> x y ? /intr_inj; lia. - by move=> x y; rewrite ler_int; lia. Qed.
imports: elpi(elpi) Coq(QArith) Coq.micromega(OrderedRing RingMicromega) mathcomp(all_ssreflect ssralg ssrnum ssrint) mathcomp.zify(ssrZ zify)