proposition: Lemma card_mod_10_9: \10c = \1c %c[mod \9c].
proof: Proof. have nnz:= card9_nz. rewrite - succ_zero; apply:(eqmod_succ NS9 nnz NS9 NS0). move: (crem_prop NS9 nnz NS1 NS0). by rewrite (cprod1r (CS_nat NS9)) (csum0r (CS_nat NS9)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)