proposition: Lemma parallel_existence1 : forall A B P, A <> B -> exists Q, Par A B P Q.
proof: Proof. intros. assert (T:= parallel_existence A B P H). decompose [and ex] T;clear T. elim (eq_dec_points x P);intro. subst. exists x0. intuition. exists x. apply par_right_comm. apply par_col_par with x0; Par. Col. Qed.
imports: GeoCoq.Tarski_dev.Ch11_angles