proposition: Lemma ltR_total x y : x != y -> x < y \/ y < x.
proof: Proof. by case: (leR_total x y) => leyx neq_xy; [left | right] => lexy; case: neq_xy. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div order) mathcomp(ssralg ssrnum ssrint rat intdiv) Coq(Morphisms Setoid) fourcolor(real realsyntax)