proposition: Lemma col2_par__col4 : 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 /\ Col A C D /\ Col B C D.
proof: Proof. intros. destruct (not_strict_par A B C D X); trivial. apply par_symmetry in H. destruct (not_strict_par C D A B X); trivial. repeat split; Col. Qed.
imports: GeoCoq.Tarski_dev.Ch11_angles