proposition: Lemma ordinal_o_wor x: ordinalp x -> worder (ordinal_o x).
proof: Proof. move=> ox. have [pa pb]:= (sub_osr x). apply: (worder_prop_rev pa); rewrite pb => y yE nex. have p1:= (Os_sub (Os_ordinal ox) yE). have hh: sub y (substrate (sub_order x)) by ue. have ix:= (ordinal_setI nex p1); ex_tac => z zy. by apply/ordo_leP;split; [apply: yE | apply: yE | apply: setI_s1 ]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)