proposition: Lemma exercise1_3 X A B (compl := fun z => X -s z) : sub A X -> sub B X -> ((sub (compl B) A <-> sub (compl A) B) /\ (sub B (compl A) <-> sub A (compl B))).
proof: Proof. have aux1: forall a b, sub a X -> sub b X -> (sub (compl a) b <-> a \cup b = X). move => a b aX bX; split. move => s1; set_extens t; first by case /setU2_P => ts; fprops. rewrite - (setU2_Cr aX); case /setU2_P => ts; fprops. by rewrite /compl => <- t /setC_P [/setU2_P] []. have aux2: forall a b, sub a X -> sub b X -> (sub b (compl a) <-> a \cap b = emptyset). move => a b aX bX; split. move => s1; apply /set0_P =>t /setI2_P [ta tb]. by move /setC_P: (s1 _ tb) => []. move => abe t tb; apply /setC_P; split; fprops. move => ta; empty_tac1 t. move => ax bx; split. apply: (iff_trans (aux1 _ _ bx ax)); rewrite setU2_C. by apply: iff_sym; apply/aux1. apply: (iff_trans (aux2 _ _ ax bx)); rewrite setI2_C. by apply: iff_sym; apply/aux2. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)