proposition: Lemma ltR01 : (0 : R) < 1.
proof: Proof. case/ltR_total: neqR10 => // lt10 le10; case: lt10. have{le10} le0N1: (0 : R) <= -1 by rewrite -oppR0 leR_opp2. by have:= Real.mul_monotone R le0N1 le0N1; rewrite mulR0 mulN1R oppRK. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div order) mathcomp(ssralg ssrnum ssrint rat intdiv) Coq(Morphisms Setoid) fourcolor(real realsyntax)