proposition: Lemma card_prod_3_3: \3c *c \3c = \9c.
proof: Proof. have aux n: natp n -> csucc (csucc (csucc n)) = n +c \3c. move => nN; rewrite /card_three (csum_nS _ NS2) - succ_one (csum_nS _ NS1). by rewrite (Nsucc_rw nN). rewrite [card_nine] (aux _ NS6) [card_six] (aux _ NS3). rewrite{2} /card_three (Nsucc_rw NS2) cprodDr (cprod1r (CS_nat NS3)). by rewrite cprodC csum_nn. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)