proposition: Lemma example_is_worder a b: worder_on (example_worder a b) (doubleton a b).
proof: Proof. have gc:sgraph (example_worder a b). move => t /set3_P; case => ->; fprops. have subs: substrate (example_worder a b) = doubleton a b. set_extens x. case/(substrate_P gc)=> [] [y]. move / (example_worder_gleP a b x y); case; case => ->; fprops. move /(example_worder_gleP a b y x); case; case => _ ->; fprops. case /set2_P=> h; have aux: (related (example_worder a b) x x) by apply/(example_worder_gleP a b x x); in_TP4. substr_tac. substr_tac. have pa: related (example_worder a b) a a by apply/example_worder_gleP; in_TP4. have pb: related (example_worder a b) b b by apply/example_worder_gleP; in_TP4. have pc: related (example_worder a b) a b by apply/example_worder_gleP; in_TP4. have oc: (order (example_worder a b)). split => //. by red;rewrite subs => y /set2_P [] ->. move=> x y z/example_worder_gleP; case; move => [ -> ->]//. move /example_worder_gleP; case; move => [ h ->] //. move=> x y /example_worder_gleP; case;move => [ -> ->] //. by move /example_worder_gleP; case; case. split; [split; [ exact | ] | exact ]. move => x xab nex. case: (inc_or_not a x)=> hyp. exists a; red; rewrite (iorder_sr oc xab); split=>//. move=> y yx; apply /(iorder_gle0P _ hyp yx); apply /example_worder_gleP. move: (xab _ yx); rewrite subs; case /set2_P; in_TP4. move: nex=> [y yx]; exists y; red;rewrite (iorder_sr oc xab); split=>//. move => z zx; apply /(iorder_gle0P _ yx zx); apply /example_worder_gleP. rewrite subs in xab. case /set2_P: (xab _ yx) => yb; first by case: hyp; rewrite -yb. case /set2_P: (xab _ zx) => zb; first by case: hyp; rewrite - zb. in_TP4. Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)