proposition: Lemma cmodmod n p: natp n -> natp p -> p <> \0c -> n %%c p = n %c[mod p].
proof: Proof. move => nN pN pnz; move: (cdivision nN pN pnz) => [qN rN [pa pb]]. have dp: (cdivision_prop (n %%c p) p \0c (n %%c p)). by split => //; rewrite cprod0r (Nsum0l rN). by rewrite - (proj2 (cquorem_pr rN pN NS0 rN dp)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)