proposition: Lemma cdivides_diff1 x a b: natp b -> x %|c a -> x %|c (a +c b) -> x %|c b.
proof: Proof. move => bN ha hb. move:(ha) => [aN xN _]. move:(Nsum_M0le b aN) => le1. by move:(proj31 (cdivides_diff le1 hb ha)); rewrite csumC cdiff_pr1. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)