proposition: Lemma qleT_ee a b: ratp a -> ratp b -> a <=q b \/ b <=q a.
proof: Proof. move: BQor_tor => [_]; rewrite BQor_sr => h pa pb. by case: (h _ _ pa pb)=> h1; [left | right]; apply /BQle_P. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)