proposition: Lemma continuity : continuityP Point Bet.
proof: Proof. unfold continuityP; intros Xi Upsilon. elim (classic (Xi P0)); intro HXiP0; elim (classic (Xi P1)); intro HXiP1; elim (classic (Xi P2)); intro HXiP2; elim (classic (Upsilon P0)); intro HUpsilonP0; elim (classic (Upsilon P1)); intro HUpsilonP1; elim (classic (Upsilon P2)); intros HUpsilonP2 [A H]; destruct A; try (exfalso; try assert (HP0P0 := H _ _ HXiP0 HUpsilonP0); try assert (HP0P1 := H _ _ HXiP0 HUpsilonP1); try assert (HP0P2 := H _ _ HXiP0 HUpsilonP2); try assert (HP1P0 := H _ _ HXiP1 HUpsilonP0); try assert (HP1P1 := H _ _ HXiP1 HUpsilonP1); try assert (HP1P2 := H _ _ HXiP1 HUpsilonP2); try assert (HP2P0 := H _ _ HXiP2 HUpsilonP0); try assert (HP2P1 := H _ _ HXiP2 HUpsilonP1); try assert (HP2P2 := H _ _ HXiP2 HUpsilonP2); simpl in *; contradiction); try (exists P0; intros X Y HX HY; destruct X, Y; try tauto; assert (HFalse := H _ _ HX HY); simpl in *; contradiction); try (exists P1; intros X Y HX HY; destruct X, Y; try tauto; assert (HFalse := H _ _ HX HY); simpl in *; contradiction); exists P2; intros X Y HX HY; destruct X, Y; try tauto; assert (HFalse := H _ _ HX HY); simpl in *; contradiction. Qed.
imports: GeoCoq.Meta_theory.Counter_models.Planar.independence Classical