proposition: Lemma proclus : euclidP Point Bet.
proof: Proof. unfold euclidP, Par. intros A B C D P Q [Hpar | Hpar]. unfold Par_strict in Hpar. destruct Hpar as [ AB_neq [ CD_ned [_ Ncol]]]. exfalso. apply Ncol. 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). intros. exists P. destruct Hpar as [ AB_neq [ CD_ned [Col_ACD Col_BCD]]]. split. apply col_alt_def; tauto. apply col_alt_def. apply col_alt_def in H. destruct H as [ ? | [ ? | ? ]]; try tauto ; subst. apply col_alt_def in Col_BCD. destruct Col_BCD as [ ? | [ ? | ?]]; subst ; tauto. apply col_alt_def in Col_ACD. destruct Col_ACD as [ ? | [ ? | ?]]; subst ; tauto. Qed.
imports: GeoCoq.Meta_theory.Counter_models.Planar.independence