proposition: Lemma FSORaddon : @SORaddon F 0 1 +%R *%R (fun x y => x - y) -%R eq (fun x y => x <= y) Q 0%Q 1%Q Qplus Qmult Qminus Qopp Qeq_bool Qle_bool R_of_Q nat nat_of_N (@GRing.exp F).
proof: Proof. apply: mk_SOR_addon. - exact: FQ. - exact: Rpower. - by move=> x y; rewrite R_of_Q_eq => /eqP. - by move=> x y; rewrite R_of_Q_le. Qed.
imports: elpi(elpi) Coq(QArith) Coq.micromega(OrderedRing RingMicromega) mathcomp(all_ssreflect ssralg ssrnum ssrint) mathcomp.zify(ssrZ zify)