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