proposition: Lemma qleT_ell a b: ratp a -> ratp b -> [\/ a = b, a <q b | b <q a].
proof: Proof. move => aq bq; case: (equal_or_not a b); first by constructor 1. by move => na; case: (qleT_ee aq bq)=> h1; [constructor 2 | constructor 3]; split => //; apply: nesym. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)