proposition: Lemma cardinal_pair : forall x y : E, ~ Equal x y -> cardinal (union (single x) (single y)) 2.
proof: Proof. intros. apply cardinal_add with (single x) y; auto with algebra. Qed.
imports: Union Singleton Diff Classical_Prop