proposition: Lemma col_cong_cong : forall A B C D, Col A B C -> Col A B D -> Cong A B C D -> Cong A C B D \/ Cong A D B C.
proof: Proof. intros. induction(eq_dec_points A B). subst B. apply cong_symmetry in H1. apply cong_identity in H1. subst D. left. Cong. induction(eq_dec_points C D). subst D. apply cong_identity in H1. subst B. right. Cong. apply par_cong_cong. right. repeat split; ColR. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel_inter_dec GeoCoq.Tarski_dev.Annexes.Tagged_predicates