proposition: Lemma BZquo_cN a b: natp a -> natp b -> (BZ_of_nat a) %/z (BZ_of_nat b) = BZ_of_nat (a%/c b).
proof: Proof. move => aN bN. rewrite /BZquo - lock /BZquo_int /BZ_of_nat /int_pp !pr1_pair !pr2_pair. by Ytac0; Ytac0;Ytac h => //; rewrite(pr1_def h) cquo_zero. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)