proposition: Lemma cdivision_of_zero n: natp n -> (n %|c \0c /\ \0c %/c n = \0c).
proof: Proof. move: NS0 => n0 aN; rewrite /cdivides. have aux: \0c = n *c \0c by rewrite cprod0r. case: (equal_or_not n \0c) => anz. by rewrite anz cquo_zero crem_zero. by move: (cquorem_pr0 n0 aN n0 anz aux) => [p1 p2]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)