proposition: Lemma card_mod_10_3: \10c = \1c %c[mod \3c].
proof: Proof. rewrite /card_ten (Nsucc_rw NS9) - card_prod_3_3. exact: (crem_prop NS3 card3_nz NS3 NS1). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)