proposition: Lemma BZdvds_pr0 a b: b %|z a -> (BZ_val b) %|c (BZ_val a).
proof: Proof. move => [az bz etc]. move: (BZdiff_diag_rw az (ZSp bz (ZS_quo az bz)) etc). move => h; move: (f_equal P h); rewrite BZprod_val => ->. by apply: cdivides_pr1; apply: BZ_valN => //;apply:ZS_quo. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)