proposition: Lemma diff_bet_ex3 : forall A B C, Bet A B C -> exists D, A <> D /\ B <> D /\ C <> D /\ Col A B D.
proof: Proof. intros. induction (eq_dec_points A B). induction (eq_dec_points B C). assert (exists D, Bet B C D /\ C <> D). apply point_construction_different. ex_and H2 D. exists D. repeat split. subst C. subst A. assumption. subst A. subst C. assumption. assumption. unfold Col. left. subst A. subst C. assumption. assert (exists D, Bet B C D /\ C <> D). apply point_construction_different. ex_and H2 D. exists D. repeat split. intro. subst D. apply between_symmetry in H. apply H1. eapply between_equality. apply H2. apply H. intro. subst D. subst A. apply between_identity in H2. apply H3. subst B. reflexivity. assumption. unfold Col. left. eapply outer_transitivity_between. apply H. apply H2. assumption. induction (eq_dec_points B C). subst C. cut(exists D : Tpoint, A <> D /\ B <> D /\ Col A B D). intro. ex_and H1 D. exists D. repeat split. assumption. assumption. assumption. assumption. apply diff_col_ex. assert (exists D, Bet B C D /\ C <> D). apply point_construction_different. ex_and H2 D. exists D. repeat split. intro. subst D. assert (B = C). eapply between_equality. apply H2. apply between_symmetry. assumption. apply H1. assumption. intro. subst D. apply between_identity in H2. subst C. apply H1. reflexivity. assumption. unfold Col. left. eapply outer_transitivity_between. apply H. assumption. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch05_bet_le