proposition: Lemma card_increasing_rev3_Nat f (r := Nat_order) (n := least_stationary f): inc f (functions_incr r (opp_order r)) -> natp n /\ forall i, natp i -> n <=c i -> Vf f i = Vf f n.
proof: Proof. move => /card_increasing_rev2_Nat [m qa qb]. rewrite /n/least_stationary ; set E := Zo _ _. have seN: sub E Nat by apply: Zo_S. have nee: nonempty E by exists m; apply: Zo_i. move: (inf_Nat seN nee). rewrite -/n; move => [/Zo_P[nN qc] qd]; split => //. Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)