proposition: Lemma card_increasing_rev5_Nat f (r := Nat_order): inc f (functions_incr r (opp_order r)) -> inc (rest_to_stationary f) functions_incr_Nat_aux.
proof: Proof. move => ha. move: (proj1 (card_increasing_rev3_Nat ha)); rewrite /natp => nN. apply/setUb_P; aw; ex_tac; rewrite LgV//. by apply/functionsP; apply:restriction2_prop; apply: card_increasing_rev4_Nat. Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)