proposition: Lemma qlt_cZ a b: intp a -> intp b -> (a <z b <-> BQ_of_Z a <q BQ_of_Z b).
proof: Proof. move => az bz; split; move => [ha hb];split. + by apply / qle_cZ. + by move/pr1_def. + by apply / qle_cZ. + by dneg h; rewrite h. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)