Skip to content

Instantly share code, notes, and snippets.

@codyroux

codyroux/no_middle.v

Created September 4, 2022 01:02
Show Gist options
  • Save codyroux/2c58f48fd90c957c891b8cb25fc8849f to your computer and use it in GitHub Desktop.
Save codyroux/2c58f48fd90c957c891b8cb25fc8849f to your computer and use it in GitHub Desktop.
Download ZIP
Raw
no_middle.v
Notation "P ≢ Q" := (~(P <-> Q))(at level 100).
Theorem no_middle : ~(exists P, (P ≢ True) /\ (P ≢ False)).
Proof.
intro h.
destruct h as [P [h1 h2]].
apply h2.
split; [ | intros h; contradiction].
intros h3.
apply h1; split; auto.
Qed.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment