proposition: Lemma Complement_injective (X : Type) : injective (@Complement X).
proof: Proof. red; intros. rewrite <- (Complement_Complement _ x). rewrite <- (Complement_Complement _ y). rewrite H. reflexivity. Qed.
imports: ZornsLemma(FunctionProperties) Coq(RelationClasses)