proposition: Lemma div3_props: [/\ \0c %%c \3c = \0c, \1c %%c \3c = \1c& \2c %%c \3c = \2c].
proof: Proof. have ha := NS3. have hb:= (cltS NS2). have hc:= (clt_ltT clt_12 hb). have hd:= (clt_ltT clt_01 hc). by split; symmetry;apply:crem_small. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)