proposition: Lemma div3_vals n (m := n %%c \3c): natp n -> [\/ m = \0c, m = \1c | m = \2c].
proof: Proof. move => nN. move: (cdivision nN NS3 card3_nz) => []; rewrite -/m => _ mN [_ m3]. case: (equal_or_not m \2c) => m2; first by constructor 3. move /(cltSleP NS2): m3 => l2; case: (clt2 (conj l2 m2)) => h; in_TP4. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)