proposition: Lemma par_not_col_strict : forall A B C D P, Par A B C D -> Col C D P -> ~Col A B P -> Par_strict A B C D.
proof: Proof. intros. induction H. assumption. spliter. exfalso. apply H1. apply (col3 C D); Col. Qed.
imports: GeoCoq.Tarski_dev.Ch11_angles