proposition: Lemma cdivides_trans2 a b c: natp c -> b %|c a -> b %|c (a *c c).
proof: Proof. move=> cN ba. have aN: (inc a Nat) by move: ba => [h _]. have aux:= (cdivides_pr1 cN aN). apply: (cdivides_trans aux ba). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)