proposition: Lemma card_increasing_rev6_Nat (r := Nat_order): (functions_incr r (opp_order r)) <=s functions_incr_Nat_aux.
proof: Proof. exists (Lf rest_to_stationary (functions_incr r (opp_order r)) functions_incr_Nat_aux). saw; apply: lf_injective. apply: card_increasing_rev5_Nat. move => u v hu hv. move: (card_increasing_rev3_Nat hu). move: (card_increasing_rev3_Nat hv). set nu := (least_stationary u); set nv := (least_stationary v). move =>[qa qb ][qc qd]. move: (card_increasing_rev4_Nat hu)(card_increasing_rev4_Nat hv) => axu axv. rewrite/rest_to_stationary => sva. move: (f_equal source sva). rewrite/restriction2; aw. move /(csucc_inj (CS_nat qc) (CS_nat qa)) => sn. move: Nat_order_wor =>[wor sr]; move: (proj1 wor) => or. case/Zo_P: hu; case/Zo_P: hv. rewrite(proj2 (opp_osr or)) sr; move/functionsP => [fv sv tv] _. move/functionsP => [fu su tu] _. apply: function_exten => //; try ue. have Ha i: i <=c nu -> Vf u i = Vf v i. move => li; move: (f_equal (Vf ^~ i) sva). have iu: inc i (csucc nu) by apply/ NleP. have iv: inc i (csucc nv) by ue. by rewrite (restriction2_V axu iu)(restriction2_V axv iv). rewrite su => i iN. case: (NleT_ee iN qc); first by apply: Ha. move => le1; move: (le1); rewrite sn => le2. rewrite (qd _ iN le1) (qb _ iN le2) Ha sn //; fprops. Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)