proposition: Lemma card_increasing_rev_Nat (r := Nat_order): cardinal (functions_incr r (opp_order r)) = aleph0.
proof: Proof. move /eq_subset_cardP1: card_increasing_rev6_Nat => /= => ha. move /eq_subset_cardP1: card_increasing_rev1_Nat; rewrite - aleph0_pr1 => hc. move /countableP: card_functions_incr_Nat_aux => hb. exact: (cleA (cleT ha hb) hc). Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)