proposition: Lemma rleT_ell a b: realp a -> realp b -> [\/ a = b, a <r b | b <r a].
proof: Proof. move => ar br; case: (equal_or_not a b); first by constructor 1. by move => nab; case: (rleT_ee ar br)=> h1; [constructor 2 | constructor 3]; split => //; apply: nesym. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)