proposition: Lemma l6_21 : forall A B C D P Q, ~ Col A B C -> C<>D -> Col A B P -> Col A B Q -> Col C D P -> Col C D Q -> P=Q.
proof: Proof. intros. elim (eq_dec_points P Q); intro; try assumption. cut False. intro; intuition. apply not_col_distincts in H. spliter. assert (Col C P Q) by (apply col_transitivity_1 with D; Col). assert (Col Q B C). induction (eq_dec_points Q A). subst; apply col_transitivity_1 with P; Col. apply col_transitivity_1 with P; Col; apply col_permutation_1, col_transitivity_1 with A; Col. assert (Col A B C). induction (eq_dec_points Q A). subst Q; assumption. induction (eq_dec_points Q B). subst; apply col_permutation_2; apply col_transitivity_1 with P; Col. apply col_permutation_2; apply col_transitivity_1 with Q; Col. contradiction. Qed.
imports: GeoCoq.Tarski_dev.Ch05_bet_le