proposition: Lemma card_increasing_rev4_Nat f (r := Nat_order): inc f (functions_incr r (opp_order r)) -> restriction2_axioms f (csucc (least_stationary f)) Nat.
proof: Proof. move: Nat_order_wor =>[wor sr]; move: (proj1 wor) => or. move => ha. move: (proj1 (card_increasing_rev3_Nat ha)) => nN. case/Zo_P: ha. rewrite(proj2 (opp_osr or)) sr; move/functionsP => [ff sf tf] _; split. - done. - rewrite sf; exact: (NS_inc_nat (NS_succ nN)). - by rewrite tf. - by rewrite - tf; apply: fun_image_Starget1. Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)