proposition: Lemma weid_comp_prop: [/\ forall x y z, weird_comp x y z -> weird_comp y x z -> x = y, forall x y z, weird_comp x y z -> weird_comp x x z /\ weird_comp y y z, forall x y z, weird_comp x y z -> weird_comp y z z -> weird_comp x z z & exists z, ~ (order_r (fun x y => weird_comp x y z))].
proof: Proof. have ra: forall x y z, weird_comp x y z -> weird_comp y x z -> x = y. by move => x y z [qa _][qb _]; apply: extensionality. have rb: forall x y z, weird_comp x y z -> weird_comp x x z /\ weird_comp y y z. by move => x y z [qa _]; split; split => //; constructor 3. have rc: forall x y z, weird_comp x y z -> weird_comp y z z -> weird_comp x z z. move => x y z [qa qb][qc qd]; split; first by apply: (sub_trans qa qc). by constructor 4. pose f z := (fun x y => weird_comp x y z). have rd: forall z, transitive_r (f z) -> order_r (f z). move => z af; split => // x y; [apply: ra | apply: rb]. have re: ~ transitive_r (f C3). have ha: f C3 C0 C1 by split; [fprops | constructor 1]. have hb: f C3 C1 C2. split; first by move => t /set1_P ->; apply/set2_P; left. by constructor 2. move:C2_ne_C01 C3_ne_C012 => [/nesym na nb][_ _ /nesym nc]. move => h; move: (h C1 C0 C2 ha hb) => [_]; case => //. - move => [_] //. - by move => [hd _]; case: C0_ne_C1. by split => //; exists C3; case => tr _ _; case:re. Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)