proposition: Lemma qleT_el a b: ratp a -> ratp b -> a <=q b \/ b <q a.
proof: Proof. move=> aq bq; case: (qleT_ell aq bq). - by move=> ->; left; BQo_tac. - by move => [pa _]; left. - by right. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)