proposition: Lemma ordinal_le_P0 x y: ordinal_leD1 x y <-> [/\ ordinalp x, ordinalp y & sub x y].
proof: Proof. split; last first. move => [ox oy sxy];split => //. split; fprops; rewrite ordinal_o_sr. exists (identity x), x; split => //. have ->: induced_order (ordinal_o y) x = (ordinal_o x). set_extens t. by move => /setI2_P [] /Zo_P [pa pb] pc; apply: Zo_i. move =>/ Zo_P [pa pb]; apply/setI2_P;split => //; apply: Zo_i => //. by apply: (setX_Slr sxy sxy). rewrite - {1} (ordinal_o_sr x); apply: identity_is; fprops. move /ordinal_le_P => [ox oy [f [S [sS oi]]]]; split => //. move: (ordinal_o_wor oy) => woy. have [p1 p2 p3]: [/\ sub S y, ordinalp S & (induced_order (ordinal_o y) S) = ordinal_o S]. case: (well_ordered_segment woy sS). move ->;rewrite iorder_substrate; [ by rewrite ordinal_o_sr; split| fprops]. move=> [u]; rewrite ordinal_o_sr => uy. move: (ordinal_transitive oy uy) => suy. rewrite ordinal_segment // => ->. split => //; first exact:(Os_ordinal oy uy). set_extens t; first by move/setI2_P => [] /Zo_P [pa pb] pc;apply /Zo_P; split. move/Zo_P =>[pa pb]; apply/setI2_i => //. by apply: Zo_i => //;apply:(setX_Sll suy). rewrite p3 in oi. by rewrite (proj1 (ordinal_isomorphism_unique ox p2 oi)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)