proposition: Lemma cdivides_itself n: natp n -> n %|c n.
proof: Proof. move=> aN; case: (equal_or_not n \0c) => nz. by rewrite {2} nz; apply:cdivides_zero. exact:(proj1 (cdivision_itself aN nz)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)