proposition: Lemma finite_total_enum r (f := (the_ordinal_iso r)) (n := cardinal (substrate r)): total_order r -> finite_set (substrate r) -> [/\ natp n, bijection_prop f n (substrate r), forall i j, i <c n -> j <c n -> (i <=c j <-> gle r (Vf f i) (Vf f j)), forall i j, i <c j -> j <c n -> glt r (Vf f i) (Vf f j) & forall i, natp i -> csucc i <c n -> glt r (Vf f i) (Vf f (csucc i))].
proof: Proof. move => ha hb. move: (finite_set_torder_wor ha hb) => wor. move:(the_ordinal_iso1 wor); rewrite -/f; move =>[on pr fp fsi]. have nN: natp n by apply/card_finite_setP. move: fp; rewrite ordinal_o_sr => fp. have eq1: cardinal (ordinal r) = n by move/card_eqP : (equipotent_bp fp). have fsp: finite_set (ordinal r) by apply/card_finite_setP; rewrite eq1. move: (card_card (CS_finite_o (ordinal_finite1 (OS_ordinal wor) fsp))). rewrite eq1 => rb. rewrite - rb in fp. move:(fp) =>[[[_ qa] _] sf tf]. have rc i j: i <c n -> j <c n -> (i <=c j <-> gle r (Vf f i) (Vf f j)). move => lin ljn; move:(proj31_1 lin) (proj31_1 ljn) => co cij. move/(NltP nN):lin => lin; move /(NltP nN): ljn => ljn. move: (fsi i j); rewrite sf => fs. move:(fs lin ljn) (ordo_leP (ordinal r) i j); rewrite - rb => Ha Hb. split; first by move => /proj33 h; apply/ Ha/Hb. by move=> /Ha/Hb /proj33 h. have rd i j: i <c j -> j <c n -> glt r (Vf f i) (Vf f j). move => [lij nij] ljn; move: (cle_ltT lij ljn) => lion. have isf: inc i (source f) by rewrite sf; apply/NltP. have jsf: inc j (source f) by rewrite sf; apply/NltP. by split; [ apply/rc | move/(qa _ _ isf jsf)]. by split => // i iN lsi; apply: rd => //; apply: cltS. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)