proposition: Lemma Rtrichotomy_inf:forall r1 r2 : R, {(r1 < r2)%R} + {r1 = r2} + {(r2<r1)%R}.
proof: Proof. intros r1 r2; elim (total_order_T r1 r2); intros ;auto. Qed.
imports: Coq(Reals) Coq(Lra) Coq(Fourier) Coq(Euclid) Coq(Lia)