proposition: Lemma ord_omega_pr: ordinal Nat_order = omega0.
proof: Proof. have bwo := proj1 Nat_order_wor. suff: (ordinal_o omega0 = Nat_order). by move => <-; apply: ordinal_o_o; fprops. apply: order_exten;fprops. move => u v; split. move /graph_on_P1 => [p1 p2 p3]; apply Nat_order_leP. by split => //;split; fprops. by move/Nat_order_leP => [pa pb [_ _ pc]];apply /graph_on_P1. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)