proposition: Lemma double_mod3 n: natp n -> (n %%c \3c = \0c <-> (cdouble n) %%c \3c = \0c).
proof: Proof. have [sa sb sc]:=div3_props. move => nN. move: (crem_prod NS3 card3_nz NS2 nN); rewrite sc => H. split => hb; first by move: H; rewrite /eqmod hb cprod0r sa. move: H; rewrite /eqmod -/(cdouble n) hb; case: (div3_vals nN) => // ->. by rewrite (cprod1r CS2) sc => h; case: card2_nz. by rewrite cprod_22 (proj2 div3_props2) => h ; case: card1_nz. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)