proposition: Lemma EnsembleProduct_Complement {X Y : Type} (U : Ensemble X) (V : Ensemble Y) : Complement (EnsembleProduct U V) = Union (EnsembleProduct Full_set (Complement V)) (EnsembleProduct (Complement U) Full_set).
proof: Proof. apply Extensionality_Ensembles; split; red; intros. - red in H. red in H. apply not_and_or in H. destruct x as [x y]. destruct H. + right. split; [assumption|constructor]. + left. split; [constructor|assumption]. - destruct H. + destruct x, H. cbv. intros. intuition. + destruct x, H. cbv. intuition. Qed.
imports: ZornsLemma(EnsemblesImplicit InverseImage)