proposition: Lemma C2_ne_C01: C2 <> C0 /\ C2 <> C1.
proof: Proof. split => h; first by move: inc_C0_C2; rewrite h /C0; case; case. move: inc_C1_C2; rewrite h; move /set1_P; fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)