proposition: Corollary incomparable_C_D_inconsistent: False.
proof: Proof. enough (c ∈ W) as contra. { rewrite Wc in contra. destruct contra as [_ [ ]%irreflexivity]. } apply W'_le_W. now right. Qed.
imports: Coq(Relations Equivalence Morphisms Utf8) Coq(ChoiceFacts ClassicalFacts) Coq.Program(Basics) Coq.Logic(SetoidChoice)