proposition: Lemma card_sincreasing_rev_Nat (r := Nat_order) : functions_sincr r (opp_order r) = emptyset.
proof: Proof. move: Nat_order_wor =>[wor sr]; move: (proj1 wor) => or. apply/set0_P => [f /Zo_P[ha hb]]. move:(strict_increasing_fun_reva hb). rewrite /opp_order (igraph_involutive (proj41 or)). move => [_ _ [ff sf tf] fi]. have hc i: inc i (substrate Nat_order) -> inc (Vf f i) (substrate Nat_order). rewrite -{1} sf - tf => isg; Wtac. move: (worder_decreasing_finite wor wor hc fi); rewrite sr => fn. by move: (finite_not_infinite_set fn infinite_Nat). Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)