proposition: Lemma parallel_existence : forall A B P, A <> B -> exists C, exists D, C<>D /\ Par A B C D /\ Col P C D.
proof: Proof. intros. induction(col_dec A B P). exists A. exists B. repeat split. assumption. Par. Col. assert(exists P', Col A B P' /\ Perp A B P P'). eapply l8_18_existence. assumption. ex_and H1 P'. assert(P <> P'). intro. subst P'. contradiction. induction(eq_dec_points P' A). subst P'. assert(exists Q, Per Q P A /\ Cong Q P A B /\ OS A P Q B). eapply ex_per_cong. auto. assumption. apply col_trivial_2. intro. apply H0. Col. ex_and H4 Q. exists P. exists Q. assert(P <> Q). intro. treat_equalities. intuition. repeat split. assumption. apply l12_9 with P A; Cop. apply per_perp_in in H4. apply perp_in_perp_bis in H4. induction H4. apply perp_distinct in H4. spliter. absurde. apply perp_left_comm. assumption. auto. assumption. Col. assert(exists Q, Per Q P P' /\ Cong Q P A B /\ OS P' P Q A). eapply ex_per_cong. auto. assumption. Col. intro. apply H0. eapply (col_transitivity_1 _ P'). auto. Col. Col. ex_and H5 Q. exists P. exists Q. assert(P <> Q). intro. treat_equalities. intuition. repeat split. assumption. apply l12_9 with P P'. exists P; left; split; Col. Cop. exists P; left; split; Col. apply coplanar_perm_3, col_cop__cop with A; Col; Cop. apply H2. apply per_perp_in in H5. apply perp_in_perp_bis in H5. induction H5. apply perp_distinct in H5. spliter. absurde. apply perp_left_comm. assumption. auto. assumption. Col. Qed.
imports: GeoCoq.Tarski_dev.Ch11_angles