proposition: Lemma setC_decreasing E: strict_decreasing_fun (Lf (complement E)(\Po E)(\Po E)) (subp_order E) (subp_order E).
proof: Proof. move: (subp_osr E); set (r:=sub_order E); move => [or sr]. have ta: lf_axiom (complement E) (\Po E) (\Po E). move=> c cE;apply/setP_P; apply: sub_setC. split => //; first by hnf; aw; split => //; apply: lf_function. move=> x y [] /subp_gleP [xE yE xy] nxy. rewrite !LfV //; try (apply/setP_P => //); split. apply/subp_gleP;split; try (apply:sub_setC); by apply /(set_CSm xE yE). dneg cc; move:(f_equal (complement E) cc). by rewrite (setC_K yE) (setC_K xE). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)