proposition: Lemma RF F : @field_theory F 0 1 +%R *%R (fun x y => x - y) -%R (fun x y => x / y) GRing.inv eq.
proof: Proof. by split=> // [||x /eqP]; [exact: RR | exact/eqP/oner_neq0 | exact: mulVf]. Qed.
imports: elpi(elpi) Coq(QArith) Coq.micromega(OrderedRing RingMicromega) mathcomp(all_ssreflect ssralg ssrnum ssrint) mathcomp.zify(ssrZ zify)