proposition: Lemma C4_P x: inc x C4 <-> [\/ x = C0, x = C1, x = C2 | x = C3].
proof: Proof. split. case /setU1_P; last (by constructor 4); by case /C3_P; in_TP4. case => ->; apply/setU1_P; last (by right); left; apply /C3_P; in_TP4. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)