proposition: Lemma C3_ne_C012: [/\ C3 <> C0, C3 <> C1 & C3 <> C2].
proof: Proof. have pa: inc C0 C3 by apply/C3_P; constructor 1. have pb: inc C1 C3 by apply/C3_P; constructor 2. have pc: inc C2 C3 by apply/C3_P; constructor 3. move:C2_ne_C01 => [pd pe]. split => h; first by move: pa ; rewrite h; case; case. by move: pb ; rewrite h; move/set1_P; fprops. move: pc; rewrite h; case/set2_P; fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)