proposition: Lemma cdivision_itself a: natp a -> a <> \0c -> (a %|c a /\ a %/c a = \1c).
proof: Proof. move=> aN anz; rewrite /cdivides. have aux:= esym (cprod1r (CS_nat aN)). by move: (cquorem_pr0 aN aN NS1 anz aux) => [p1 p2]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)