proposition: Lemma Rsor : @SOR R 0 1 +%R *%R (fun x y => x - y) -%R eq Order.le Order.lt.
proof: Proof. apply: mk_SOR_theory. - exact: RelationClasses.eq_equivalence. - by move=> x _ <- y _ <-. - by move=> x _ <- y _ <-. - by move=> x _ <-. - by move=> x _ <- y _ <-. - by move=> x _ <- y _ <-. - exact: RR. - by []. - by move=> x y xley ylex; apply: le_anti; rewrite xley ylex. - by move=> x y z; apply: le_trans. - move=> x y; rewrite lt_neqAle; split. + by move=> /andP[/eqP yneqx ->]; split. + by move=> [-> /eqP ->]. - move=> x y; case: (ltgtP x y) => [xlty|yltx|<-]. + by left. + by right; right. + by right; left. - by move=> x y z; rewrite lerD2l. - exact: mulr_gt0. - by apply/eqP; rewrite eq_sym oner_neq0. Qed.
imports: elpi(elpi) Coq(QArith) Coq.micromega(OrderedRing RingMicromega) mathcomp(all_ssreflect ssralg ssrnum ssrint) mathcomp.zify(ssrZ zify)