proposition: Lemma worder_rc_ord (r:relation) : (forall x y, r x y -> x <=o y) -> (order_r r) -> (forall x y, r x x -> r y y -> (r x y \/ r y x)) -> worder_rc r.
proof: Proof. move=> h1 h2 h3; split. split => // x hx [w wx]. have ow:= (proj31 (h1 _ _ (hx _ wx))). move: (least_ordinal4 ow wx (p:=inc^~x)); set y := least_ordinal _ _. move=> [oy yx yl]; rewrite /has_least/least (graph_on_sr hx). exists y; split => //. move => t tx; apply /graph_on_P1; split => //. case: (h3 _ _ (hx _ yx) (hx _ tx)) => // /h1 ty. have ot:= (proj31 (h1 _ _ (hx _ tx))). by move: (yl _ ot tx) => yt; rewrite (oleA ty yt); apply: hx. move => x /h1 xx. have ox:= (proj31 xx). exists (Zo (osucc x) (r^~ x)); move => y;split; first by move /Zo_hi. by move => ryx; apply:Zo_i => //; apply /(oleP ox); apply: h1. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)