proposition: Lemma card_increasing_Nat_aux f (r := Nat_order) : inc f (functions_incr r r) <-> inc f (functions Nat Nat) /\ forall i j, i <=c j -> natp j -> Vf f i <=c Vf f j.
proof: Proof. move: Nat_order_wor =>[[or _] sr]. split. move => /Zo_P []; rewrite sr => ha hb; split => // i j lij jN. have la: gle Nat_order i j. apply/Nat_order_leP; split => //; apply: (NS_le_nat lij jN). by move: hb => [_ _ _ fp]; move: (fp i j la) => /Nat_order_leP/proj33. move =>[qa qb]; move/functionsP: (qa) => qc. apply: Zo_i; [ ue | split => //; first ue]. move: qc =>[ff sf tf]. move => i j /Nat_order_leP[iN jN le1]; apply/Nat_order_leP. move: (qb _ _ le1 jN) => qd. by split => //; rewrite /natp; Wtac; rewrite sf. Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)