proposition: Lemma card_increasing_rev1_Nat (r := Nat_order) : Nat <=s (functions_incr r (opp_order r)).
proof: Proof. move: Nat_order_wor =>[wor sr]; move: (proj1 wor) => or. pose c v := constant_function Nat Nat v. have ha v: natp v -> inc (c v) (functions_incr r (opp_order r)). move => vN. have sc: source (c v) = Nat by rewrite /c/constant_function; aw. have tc: target (c v) = Nat by rewrite /c/constant_function; aw. move: (constant_constant_fun Nat vN) => cp. have qa: substrate r = source (c v) by ue. have qb: substrate r = target (c v) by ue. apply/Zo_P; split. rewrite(proj2 (opp_osr or)) sr. by move: (proj1 cp) => fc; apply/functionsP. move:(proj2 (constant_fun_increasing or or qa qb cp)). by move/(decreasing_fun_reva). pose F := Lf c Nat (functions_incr r (opp_order r)). have injf: injection F. apply: lf_injective => // a b aN bN sv. move: (f_equal (Vf ^~ \0c) sv). by rewrite /c (constant_V aN NS0) (constant_V bN NS0). by exists F; rewrite /F;split => //; aw. Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)