proposition: Lemma Exercise6_33h (x := E6_33_x) (r:= E6_33_r): [/\ worder_on r M, order_isomorphism x (ordinal_o c) r & (forall a b, inc a c -> inc b c -> (a <=o b <-> gle r (Vf x a) (Vf x b)))].
proof: Proof. have oc:= (proj1 (proj1 Exercise6_33c)). move: (ordinal_o_wor oc) => wo1; move: (wo1) => [o1 _]. have sr1:= (ordinal_o_sr c). move: Exercise6_33g; rewrite -/x; move => [bx sx tx]. rewrite -{2} sx in sr1. move: (order_transportation bx (conj o1 sr1)); rewrite /x -/ E6_33_r -/r => oi1. move: (oi1) => [_ or [_ _ sr2] xinc]. have wo: worder r by apply: worder_invariance wo1; exists E6_33_x. rewrite tx in sr2; split => //. move => u v ux vx. move: (xinc u v); rewrite sx => H; apply: iff_trans (H ux vx). move: (ordo_leP c u v) => H1; split =>h. by apply/H1; split => //; case: h. by move/H1: h =>[ _ _ hØ]; split => //; apply: (Os_ordinal oc). Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)