proposition: Lemma sub_nat_isomorphism A (r := induced_order Nat_order A) : sub A Nat -> (finite_set A -> exists2 n, natp n & r \Is induced_order Nat_order n) /\ (~ finite_set A -> r \Is Nat_order).
proof: Proof. move => sub1. move:Nat_order_wor => [wor sr]. have or := proj1 wor. have sub3: sub A (substrate Nat_order) by ue. have sub2: sub r Nat_order by apply: setI2_1. move: (induced_wor wor sub3) (iorder_sr or sub3) => wor1 sr1. move: (ordinal_o_is wor1). move: (order_cp2 wor1 wor sub2); rewrite ord_omega_pr. case/ole_eqVlt. move => -> eq1; split. move:eq1 =>[f [_ _ [bf sf tf] _ ]]. move/card_finite_setP. move: (card_bijection bf); rewrite sf tf sr1 ordinal_o_sr => ->. by rewrite cardinal_Nat => h; move/(NltP h):h => /proj2. move => _. move: (ordinal_o_is wor); rewrite ord_omega_pr => is2. exact: (orderIT eq1 (orderIS is2)). move/(oltP OS_omega); rewrite -/r => h1 h2; split. move => _; exists (ordinal r) => //. have -> //:induced_order Nat_order (ordinal r) = ordinal_o (ordinal r). have ha: sub (ordinal r) omega0 by move/(oltP OS_omega): h1; case; case. move:(ha); rewrite -/Nat - sr => hb. move: (iorder_osr or hb) (ordinal_o_or (ordinal r)) =>[or2 sr2] or3. apply: order_exten => // x y; split. move/iorder_gleP=>[xa ya /Nat_order_leP[xn yn le]]. by apply/ordo_leP; split => //; case: le. move => /ordo_leP[xa ya etc]. apply/(iorder_gle0P) => //. move: (ha _ xa) (ha _ ya) => xN yN; apply/Nat_order_leP. by split => //; split => //; apply: CS_nat. case;move: h2 =>[f [_ _ [bf sf tf] _]]. apply/card_finite_setP. move: (card_bijection bf); rewrite sf tf sr1 ordinal_o_sr; move ->. by rewrite (card_card (CS_nat h1)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)