proposition: Lemma qle_cZ a b: intp a -> intp b -> (a <=z b <-> BQ_of_Z a <=q BQ_of_Z b).
proof: Proof. move => az bz. have aq: ratp (BQ_of_Z a) by apply: BQ_of_Z_iQ. have bq: ratp (BQ_of_Z b) by apply: BQ_of_Z_iQ. rewrite /BQ_le /BQle_aux /BQ_of_Z; aw; rewrite BZprod_1r //BZprod_1l //. by split => // [] []. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)