proposition: Lemma per_one_side : forall A B P Q C C', A <> P -> C' <> P -> ~Col A B C -> Col P Q A -> Col P Q C' -> Perp A B P Q -> Per C C' P -> OS A B C C'.
proof: Proof. intros. assert(A <> B). apply perp_not_eq_1 in H4. assumption. assert(P <> Q). apply perp_not_eq_2 in H4. assumption. induction (eq_dec_points C C'). subst C'. apply one_side_reflexivity. intro. apply H1. Col. assert(Perp C C' C' P). eapply per_perp_in in H5. eapply perp_in_perp_bis in H5. induction H5. apply perp_not_eq_1 in H5. tauto. assumption. auto. auto. assert(Perp C C' P Q). apply perp_sym. eapply perp_col. assumption. apply perp_sym. apply perp_right_comm. apply H9. Col. assert(Par C C' A B). eapply l12_9_2D. apply H10. assumption. assert(Par_strict C C' A B). induction H11. assumption. spliter. apply False_ind. apply H1. Col. eapply l12_6. apply par_strict_symmetry. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel_inter_dec