proposition: Lemma setC_isomorphism E: order_isomorphism (Lf (complement E)(\Po E)(\Po E)) (subp_order E) (opp_order (subp_order E)).
proof: Proof. move: (subp_osr E); set (r:=sub_order E); move => [or sr]. case: (opp_osr or); rewrite sr => or' sr'. have ta: lf_axiom (complement E) (\Po E) (\Po E). move=> c cE;apply/setP_P; apply: sub_setC. split => //. hnf; aw; split => //; apply:lf_bijective => //. by move => u v /setP_P /setC_K {2} <- /setP_P /setC_K {2} <- ->. move => y /setP_P yE; exists (E -s y); last by rewrite setC_K. apply /setP_P; apply: sub_setC. hnf;aw => x y xE yE; rewrite !LfV//. move: xE yE => /setP_P xE /setP_P yE; split. move/subp_gleP => [_ _ /(set_CSm xE yE) h]. apply/opp_gleP /subp_gleP; split =>//; apply: sub_setC. by move => /opp_gleP /subp_gleP [_ _ /(set_CSm xE yE) h]; apply/subp_gleP. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)