proposition: Lemma not_strict_par : forall A B C D X, Par A B C D -> Col A B X -> Col C D X -> Col A B C /\ Col A B D.
proof: Proof. intros. split. eapply not_strict_par1. apply H. apply H0. assumption. eapply not_strict_par2. apply H. apply H0. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch11_angles