proposition: Lemma par_strict_not_cols : forall A B C D, Par_strict A B C D -> ~ Col A B C /\ ~ Col B C D /\ ~ Col C D A /\ ~ Col A B D.
proof: Proof. intros. repeat split. apply par_strict_not_col_1 with D, H. apply (par_strict_not_col_2 A), H. apply par_strict_not_col_3 with B, H. apply par_strict_not_col_4 with C, H. Qed.
imports: GeoCoq.Tarski_dev.Ch11_angles