proposition: Theorem wordering_ole: worder_r ordinal_le.
proof: Proof. split; first split. - move=> x y z [Kx Ky xy][_ Kz yz]. by split => //; apply: sub_trans yz. - move=> x y [Kx Ky xy][_ _ yx]. by apply: extensionality. - by move=> x y [ox oy _]; split => //;split. move=> x ale nex. have alo: ordinal_set x by move=> a /ale [h _]. move: (least_ordinal0 alo nex) => [ha hb hc]. exists (intersection x); hnf; rewrite (graph_on_sr ale); split=> // a ax. by apply /graph_on_P1; split => //; apply:hc. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)