proposition: Lemma in_angle_reverse : forall A B A' C D, A' <> B -> Bet A B A' -> InAngle C A B D -> InAngle D A' B C.
proof: Proof. intros. assert (Hd := H1). apply inangle_distincts in Hd. spliter. induction (col_dec B A C). assert(HH:=or_bet_out C B A). induction HH. assert(Bet A B D). eapply bet_in_angle_bet. apply between_symmetry. apply H6. assumption. assert(Out B A' C). repeat split; try assumption. eapply l5_2. apply H2. assumption. apply between_symmetry. assumption. assert( Out B D A'). repeat split; try assumption. eapply l5_2. apply H2. assumption. assumption. apply out321__inangle. auto. apply l6_6. assumption. induction H6. repeat split; try assumption. exists B. split. unfold Out in H6. spliter. induction H8. eapply between_inner_transitivity. apply between_symmetry. apply H0. assumption. eapply outer_transitivity_between. apply between_symmetry. apply H0. assumption. auto. left. reflexivity. apply False_ind. apply H6. apply col_permutation_2. assumption. induction (col_dec B D C). assert(HH:=or_bet_out C B D). induction HH. assert(OS A B C D). apply in_angle_one_side. intro. apply H5. eapply (col_transitivity_1 _ D). auto. apply col_permutation_1. assumption. assumption. assumption. assumption. assert(TS A B C D). repeat split; try assumption. intro. apply H5. apply col_permutation_3. assumption. intro. apply H5. eapply (col_transitivity_1 _ D). auto. apply col_permutation_2. assumption. assumption. exists B. split. apply col_trivial_3. assumption. apply l9_9 in H9. contradiction. induction H7. assert(InAngle C A' B C). apply inangle3123; assumption. eapply l11_25. apply H8. apply out_trivial. auto. apply out_trivial. auto. apply l6_6. assumption. apply False_ind. apply H7. apply col_permutation_2. assumption. assert( HH:= H1). apply in_angle_two_sides in HH. assert(HH1:=H1). unfold InAngle in H1. spliter. ex_and H9 X. induction H10. subst X. apply col_in_angle; try assumption. left. repeat split; try assumption. eapply l5_2. apply H1. assumption. assumption. assert(HH0:= HH). unfold TS in HH. assert (C <> B). spliter. intro. subst B. Col. spliter. assert(OS D B C A). apply in_angle_one_side. intro. apply H12. apply col_permutation_1. eapply (col_transitivity_1 _ X). unfold Out in H10. spliter. auto. apply col_permutation_1. eapply (col_transitivity_1 _ D). intro. subst D. apply between_identity in H9. subst X. ex_and H14 T. apply between_identity in H14. subst T. contradiction. apply col_permutation_2. assumption. apply col_permutation_5. apply bet_col. assumption. apply out_col. assumption. intro. apply H13. apply col_permutation_1. assumption. apply l11_24. assumption. assert(~Col A D B). intro. apply H12. apply col_permutation_1. eapply (col_transitivity_1 _ X). unfold Out in H10. spliter. auto. apply col_permutation_1. eapply (col_transitivity_1 _ D). intro. subst D. apply between_identity in H9. subst X. apply H13. apply col_permutation_1. apply out_col. assumption. assumption. apply col_permutation_5. apply bet_col. assumption. apply out_col. assumption. assert(~Col A' D B). intro. apply H16. apply col_permutation_1. eapply (col_transitivity_1 _ A'). auto. apply col_permutation_1. apply bet_col. assumption. apply col_permutation_2. assumption. assert(TS D B A A'). repeat split; try assumption. exists B. split. apply col_trivial_3. assumption. assert(TS D B C A' ). eapply l9_8_2. apply H18. apply one_side_symmetry. assumption. unfold TS in H19. assert (~ Col C D B). spliter. assumption. spliter. ex_and H22 Y. repeat split; try assumption. exists Y. split. apply between_symmetry. assumption. right. apply col_permutation_1 in H22. unfold Col in H22. induction H22. assert(OS C B A' Y). apply out_one_side. left. intro. apply H12. apply col_permutation_1. eapply (col_transitivity_1 _ A'). auto. apply col_permutation_1. apply bet_col. assumption. apply col_permutation_1. assumption. apply l6_6. apply bet_out. intro. subst Y. apply H13. apply col_permutation_5. apply bet_col. assumption. assumption. assert(TS C B Y D). repeat split. intro. apply H20. apply col_permutation_1. eapply (col_transitivity_1 _ Y). intro. subst Y. unfold OS in H24. ex_and H24 C0. unfold TS in H26. spliter. apply H26. apply col_trivial_3. apply col_permutation_2. assumption. apply col_permutation_1. apply bet_col. assumption. intro. apply H20. apply col_permutation_4. assumption. exists B. split. apply col_trivial_3. apply between_symmetry. assumption. assert(TS C B A A'). repeat split; try assumption. intro. apply H12. apply col_permutation_1. eapply (col_transitivity_1 _ A'). auto. apply col_permutation_1. apply bet_col. assumption. apply col_permutation_2. assumption. exists B. split. apply col_trivial_3. assumption. assert(TS C B Y A). eapply l9_8_2. apply l9_2. apply H26. assumption. assert(OS C B A D). eapply l9_8_1. apply l9_2. apply H27. apply l9_2. assumption. apply l9_9 in HH0. contradiction. repeat split. intro. subst Y. apply H12. apply col_permutation_1. eapply (col_transitivity_1 _ A'). auto. apply col_permutation_1. apply bet_col. assumption. apply col_permutation_1. apply bet_col. assumption. assumption. induction H22. left. assumption. right. apply between_symmetry. assumption. intro. apply H5. assumption. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2