proposition: Lemma div3_props2: \3c %%c \3c = \0c /\ \4c %%c \3c = \1c.
proof: Proof. move: (cdivides_itself NS3) div3_props => [_ _ ha] [_ hb _]. split => //. move: (crem_sum NS3 card3_nz NS3 NS1). by rewrite /eqmod ha hb (csum0l CS1) hb -(Nsucc_rw NS3). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)