proposition: Lemma euclid : euclidP Point Bet.
proof: Proof. unfold euclidP; intros A B C D P Q HPar HC HNC HCop. exists P0; split; apply col_alt_def. { assert (H : P <> Q); [intro; subst; auto|]. destruct P, Q; simpl; try tauto; right; try (left ; split ; discriminate); right; try (left ; split ; discriminate); right; split ; discriminate. } { assert (H : C <> D). { unfold Par, Par_strict in HPar; induction HPar; spliter; auto. } destruct C, D; simpl; try tauto; right; try (left ; split ; discriminate); right; try (left ; split ; discriminate); right; split ; discriminate. } Qed.
imports: GeoCoq.Meta_theory.Counter_models.Planar.independence