proposition: Lemma Prop_contradiction_neq (P Q : Prop) (HP : P) : ~ (P /\ Q) -> P <> Q.
proof: Proof. intros ? ?. subst. tauto. Qed.
imports: Coq(ClassicalChoice Description Lia PeanoNat Program.Subset) ZornsLemma(Cardinals CountableTypes CSB DecidableDec Families Finite_sets FiniteTypes FunctionProperties FunctionPropertiesEns InverseImage Powerset_facts Proj1SigInjective ReverseMath.AddSubtract) Coq(RelationClasses)