proposition: Lemma BZrem_small a b: intp a -> intp b -> b <> \0z -> (a %%z b) <z (BZabs b).
proof: Proof. by move => pa pb pc;move: (BZdvd_correct pa pb pc) => [_ _ [ _ bb _]]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)