proposition: Lemma OT_finite_ordered r (E := substrate r): total_order r -> finite_set E -> order_type_of r = OT_of_nat (cardinal E).
proof: Proof. move => ha hb; rewrite (order_type_unique (finite_ordered_interval2 ha hb)). rewrite -/E. set n := (cardinal E). suff: (Nint_co n) = ordinal_o n by move ->. move: (Nintco_wor n) => [[or1 _] sr1]. apply: (order_exten or1 (ordinal_o_or n)). have nN: natp n by apply /NatP. move => x y; apply: (iff_trans (Nintco_gleP nN x y)); split. move => [qa qb]; move: (proj33 qa) => qc. move/(NltP nN): (cle_ltT qa qb) => xn; move/(NltP nN): qb => yn. by apply/(ordo_leP). move/(ordo_leP) =>[qa qb qc]. move/(NltP nN): qb => lyn; move/(NltP nN): qa => lxn. split => //; move: (proj31_1 lxn)(proj31_1 lyn) => cx cy //. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)