proposition: Lemma BZdvd_itself a: intp a -> a <> \0z -> (a %|z a /\ a %/z a = \1z).
proof: Proof. move => az anz. move: (BZdvds_pr1 ZS1 az) (BZdvds_pr5 az ZS1 anz). by rewrite (BZprod_1r az) (BZprod_1l az). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)