proposition: Lemma BZdvd_unique1 a b q r: intp a -> intp b -> intp q -> intp r -> b <> \0z -> BZdivision_prop a b q r -> (q = a %/z b /\ r = a %%z b).
proof: Proof. move => pa pb pc pd pe H1. move: (BZdvd_correct pa pb pe) => [pc' pd'' H2]. exact (BZdvd_unique pa pb pe pc pd pc' (BZp_sBZ pd'') H1 H2). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)