proposition: Lemma euclid : euclidP Point Bet.
proof: Proof. unfold euclidP; intros A B C D P Q HPar HC HNC HCop. destruct HPar as [HParS|[HAB [HCD [HC1 HC2]]]]. { destruct HParS as [HAB [HCD [_ HNI]]]. exfalso; apply HNI. destruct A, B, C, D; try tauto; try (exists P0; split; apply col_alt_def; tauto); try (exists P1; split; apply col_alt_def; tauto); try (exists P2; split; apply col_alt_def; tauto). } { exists P; split; apply col_alt_def; [tauto|]. apply col_alt_def in HC. destruct HC as [? | [ ? | ?]]; (try tauto); subst. { apply col_alt_def in HC2. destruct HC2 as [ ? | [ ? | ?]]; subst; tauto. } { apply col_alt_def in HC1. destruct HC1 as [ ? | [ ? | ?]]; subst ; tauto. } } Qed.
imports: GeoCoq.Meta_theory.Counter_models.Planar.independence