proposition: Lemma card_increasing_rev2_Nat f (r := Nat_order) : inc f (functions_incr r (opp_order r)) -> exists2 n, natp n & forall i, natp i -> n <=c i -> Vf f i = Vf f n.
proof: Proof. move: Nat_order_wor =>[wor sr]; move: (proj1 wor) => or. case/Zo_P. rewrite(proj2 (opp_osr or)) sr; move/functionsP => [ff sf tf]. move/(increasing_fun_reva). rewrite /opp_order (igraph_involutive (proj41 or)) => - [ _ _ _ df]. have Ha: forall i j, natp i -> natp j -> i <=c j -> Vf f j <=c Vf f i. move => i j iN jN lik. have /df/Nat_order_leP/proj33// : gle r i j by apply/Nat_order_leP. pose p n := exists2 m, natp m & n = Vf f m. have zN := NS0. set v := Vf f \0c. have pv: p v by exists \0c. have vN: natp v by rewrite /natp /v; Wtac; ue. move: (least_int_prop vN pv); set m := least_ordinal _ _. move => [mn [n nN mv] hyp]; exists n => //. move => i iN lin. move: (Ha n i nN iN lin); rewrite - mv => le1. have nw: natp (Vf f i) by apply: (NS_le_nat le1). have pw: p (Vf f i) by exists i. exact: (cleA le1 (hyp _ nw pw)). Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)