proposition: Lemma not_strict_par1 : forall A B C D X, Par A B C D -> Col A B X -> Col C D X -> Col A B C.
proof: Proof. intros. unfold Par in H. induction H. unfold Par_strict in H. spliter. assert(exists X, Col X A B /\ Col X C D). exists X. split; Col. contradiction. spliter. apply col_permutation_1. eapply col_transitivity_1. apply H2. Col. Col. Qed.
imports: GeoCoq.Tarski_dev.Ch11_angles