proposition: Lemma BZdvds_trans2 a b c: intp c -> b %|z a -> b %|z (c *z a).
proof: Proof. move => cz dv1; move: (dv1)=> [h _ _ ]. exact: (BZdvds_trans (BZdvds_pr1 cz h) dv1). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)