proposition: Lemma qleR_aux a: ratp a -> BQle_aux a a.
proof: Proof. move => /BQ_P [_ nz dzp _]; rewrite /BQle_aux BZprodC. by apply: zleR; apply:ZSp=> //; apply: BZps_sBZ. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)