proposition: Lemma diff_col_ex3 : forall A B C, Col A B C -> exists D, A <> D /\ B <> D /\ C <> D /\ Col A B D.
proof: Proof. intros. assert(cas1 := diff_bet_ex3 A B C). assert(cas2 := diff_bet_ex3 B C A). assert(cas3 := diff_bet_ex3 C A B). unfold Col in H. induction H. apply (diff_bet_ex3 A B C). assumption. induction H. assert (HH:=H). induction (eq_dec_points B C). subst C. assert (exists C, A <> C /\ B <> C /\ Col A B C). apply (diff_col_ex). ex_and H0 D. exists D. repeat split; assumption. apply cas2 in HH. ex_and HH D. exists D. repeat split; try assumption. apply col_permutation_2. eapply col_transitivity_1. apply H0. assumption. unfold Col. left. assumption. induction (eq_dec_points A C). subst C. assert (exists C, A <> C /\ B <> C /\ Col A B C). apply (diff_col_ex). ex_and H0 D. exists D. repeat split; assumption. assert (HH:=H). apply cas3 in HH. ex_and HH D. exists D. repeat split; try assumption. apply col_permutation_5. eapply col_transitivity_1. apply H0. apply col_permutation_4. assumption. unfold Col. right;right. apply between_symmetry. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch05_bet_le