proposition: Lemma finite_ordinal1 n: natp n -> ordinal (Nint_co n) = n.
proof: Proof. move=> nN. have cn: cardinalp n by fprops. have ox: ordinalp n by apply: OS_cardinal. have cnn: cardinal n = n by apply: card_card. have fs: finite_set n by apply /NatP; ue. have w1 := (Nintco_wor n). have on := (OS_ordinal (proj1 w1)). have p1 := (worder_total (ordinal_o_wor ox)). have p2 := (worder_total (ordinal_o_wor on)). have pa := (ordinal_o_sr n). have [f [_ _ [bf sf tf] _]]:= (ordinal_o_is (proj1 w1)). have : (source f) \Eq (target f) by exists f;split => //. rewrite tf sf (proj2 w1). set S := substrate _ => /card_eqP aux. have p3: substrate (ordinal_o n) \Eq S. by apply/card_eqP; rewrite pa - aux card_Nint. have fs1: finite_set (substrate (ordinal_o n)) by rewrite (ordinal_o_sr n). have [g [fiso _]] := (isomorphism_worder_finite p1 p2 fs1 p3). by symmetry;apply: (ordinal_o_isu ox on); exists g. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)