proposition: Lemma cdivides_pr a b: b %|c a -> a = b *c (a %/c b).
proof: Proof. move => [aN bN dv]. move: (cdiv_pr aN bN); rewrite dv. by rewrite (Nsum0r (NS_prod bN (NS_quo b aN))). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)