proposition: Lemma worder_decreasing_finite r r' (f:fterm): worder r -> worder r' -> (forall i, inc i (substrate r) -> inc (f i) (substrate r')) -> (forall i j, glt r i j -> glt r' (f j) (f i)) -> finite_set (substrate r).
proof: Proof. move => wo1 wo2 hyp1 hyp2. case: (emptyset_dichot (substrate r)) => Ene. rewrite Ene; apply: emptyset_finite. set A := Zo (substrate r) (fun z => finite_set (segment r z)). have neZ: nonempty A. move:(worder_least wo1 Ene) =>[x [xsr xle]]; exists x; apply: (Zo_i xsr). suff: (segment r x) = emptyset by move ->; apply: emptyset_finite. apply /set0_P => y /segmentP ys. have ysr: inc y (substrate r) by order_tac. move: (xle _ ysr) (proj1 wo1) => le1 or; order_tac. set B := fun_image A f. have sB: sub B (substrate r') by move => t /funI_P[x /Zo_S /hyp1 h ->]. have neB: nonempty B by apply: funI_setne. move: (worder_prop wo2 sB neB) =>[b /funI_P [a /Zo_P [asr sf] av] bp]. have o1 := proj1 wo1. move: (segmentc_pr o1 asr) (segmentc_segment a o1) => eq1 us. have fs2: finite_set (segmentc r a) by rewrite - eq1; apply: setU1_finite. case: (well_ordered_segment wo1 us); first by move <-. move => [c csr cv]. have cA: inc c A by apply: (Zo_i csr); rewrite - cv. have cB: inc (f c) B by apply: funI_i. move: (bp _ cB). rewrite av => / (not_le_gt (proj1 wo2)); case. apply: hyp2. apply/segmentP; rewrite - cv; fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)