proposition: Lemma ordinal_isomorphism_exists r (f := ordinal_iso r): worder r -> order_isomorphism f r (ordinal_o (target f)).
proof: Proof. move=> wor;move: (proj1 wor)=> or. move: (transfinite_defined_pr target wor) => [suf sf vf]. set E:= substrate r. have fa: function f by fct_tac. have vf1: forall a b, inc a E -> (inc b (Vf f a) <-> (exists2 u, glt r u a & b = Vf f u)). move=> a b aE; rewrite (vf _ aE) /restriction1; aw. have ssf: sub (segment r a) (source f) by rewrite sf;apply: sub_segment. split. by move/(Vf_image_P fa ssf) => [x /segmentP pa pb]; exists x. move => [x ua ub]; apply/(Vf_image_P fa ssf). by exists x => //; apply /segmentP. have incf: (forall a b, gle r a b -> sub (Vf f a) (Vf f b)). move=> a b ab t. have aE: (inc a E) by rewrite /E; order_tac. have bE: (inc b E) by rewrite /E; order_tac. move/(vf1 _ _ aE) =>[u us h]; apply/(vf1 _ _ bE); exists u => //; order_tac. have incf3: forall a b, inc a (source f) -> inc b (source f) -> sub (Vf f a) (Vf f b) -> gle r a b. rewrite sf => a b aE bE sab. case: (total_order_pr2 (worder_total wor) bE aE) => // ltab. pose (Bad:= Zo E (fun x => inc (Vf f x) (Vf f x))). have neb: nonempty Bad. by exists b;apply: (Zo_i bE); apply: sab; apply/(vf1 _ _ aE); exists b. have BE: sub Bad E by apply: Zo_S. move: (worder_prop wor BE neb) => [y /Zo_P [yE iWWy] yp]. move/(vf1 _ _ yE): (iWWy) => [u us Wu]. have badu: inc u Bad by apply: Zo_i=>//; [rewrite /E;order_tac | ue ]. move: (yp _ badu) => yu; order_tac. have injf: injection f. split=>//; move=> x y xsf ysf Wxy. have p1: sub (Vf f x) (Vf f y) by rewrite Wxy; fprops. have p2: sub (Vf f y) (Vf f x) by rewrite Wxy; fprops. move: (incf3 _ _ xsf ysf p1) (incf3 _ _ ysf xsf p2) => p3 p4; order_tac. split => //; [fprops | by rewrite ordinal_o_sr | move=> x y xsf ysf]. split; first by move => pa; apply/ordo_leP;split => //; try Wtac; apply: incf. move/ordo_leP => [_ _ xy]; apply: (incf3 _ _ xsf ysf xy). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)