proposition: Lemma cdo_wor: worder_on canonical_doubleton_order C2.
proof: Proof. have cg: sgraph canonical_doubleton_order. by move => t /set3_P; case => ->; fprops. have subs: substrate canonical_doubleton_order = C2. set_extens x. case/(substrate_P cg) => [] [y] /cdo_gleP. case;case => ->; fprops. case;case => _ ->; fprops. case /C2_P => ->; apply: (@arg1_sr _ _ C1); apply /cdo_gleP; in_TP4. have oc: (order canonical_doubleton_order). split => //. move => y;rewrite subs; case /C2_P => ->; apply /cdo_gleP; in_TP4. move=> x y z /cdo_gleP pa /cdo_gleP pb; apply /cdo_gleP. have aux: z = C0 \/ z = C1 by case: pb;move => [_ ->]; [left |right |right]. case: (equal_or_not y C0); first by move => ->; case :aux => ->; in_TP4. case: pa; move => [-> pa] //. move: pa; case: pb; move => [-> ->]; in_TP4. move=> x y /cdo_gleP pa /cdo_gleP. by case: pa; move=> [-> ->] //; case; try move => [ aa bb]. split; [ apply:(worder_prop_rev oc); rewrite subs => x xt nex | exact]. case: (inc_or_not C0 x)=> hyp. ex_tac => y yx; apply /cdo_gleP; case /C2_P: (xt _ yx) => ->; in_TP4. move: nex=> [y yx]; ex_tac. have p: forall t, inc t x -> t = C1. by move=> t tx; case/C2_P: (xt _ tx) => // ta;case: hyp; rewrite - ta. by move => t tx; apply /cdo_gleP;rewrite (p _ yx)(p _ tx); constructor 2. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)