proposition: Lemma conga_preserves_in_angle : forall A B C I A' B' C' I', CongA A B C A' B' C' -> CongA A B I A' B' I' -> InAngle I A B C -> OS A' B' I' C' -> InAngle I' A' B' C'.
proof: Proof. intros. assert(A <> B /\ C <> B /\ A' <> B' /\ C' <> B' /\ I <> B /\ I' <> B'). unfold CongA in *. spliter. repeat split; assumption. spliter. assert(HH1:= or_bet_out A B C). induction HH1. assert(Bet A' B' C'). eapply bet_conga__bet. apply H9. assumption. apply in_angle_line; assumption. induction H9. assert(Out B A I). eapply in_angle_out. apply H9. assumption. assert(Out B' A' I'). eapply l11_21_a. apply H10. assumption. apply out321__inangle. auto. assumption. assert(HH2:= or_bet_out A B I). induction HH2. assert(Bet A B C). eapply bet_in_angle_bet. apply H10. assumption. apply False_ind. apply H9. unfold Col. left. assumption. induction H10. assert(Out B' A' I'). eapply l11_21_a. apply H10. assumption. eapply col_in_angle; try assumption. left. assumption. assert(exists AA', Out B' A' AA' /\ Cong B' AA' B A). apply segment_construction_3; auto. assert(exists CC', Out B' C' CC' /\ Cong B' CC' B C). apply segment_construction_3; auto. ex_and H11 AA'. ex_and H12 CC'. assert(HH:=H1). unfold InAngle in H1. spliter. ex_and H17 J. induction H18. subst J. eapply in_angle_line; try assumption. eapply bet_conga__bet. apply H17. assumption. assert(B <> J). unfold Out in H18. spliter. auto. assert(~Col A B J). intro. apply H10. apply col_permutation_2. eapply (col_transitivity_1 _ J). assumption. apply out_col. assumption. apply col_permutation_1. assumption. assert(exists J', CongA A B J A' B' J' /\ OS A' B' J' I'). apply angle_construction_1. intro. apply H10. apply col_permutation_2. eapply (col_transitivity_1 _ J). unfold Out in H18. spliter. auto. apply out_col. assumption. apply col_permutation_1. assumption. eapply ncol_conga_ncol. apply H10. assumption. ex_and H21 J'. assert(B' <> J'). unfold CongA in H21. spliter. auto. assert(exists JJ', Out B' J' JJ' /\ Cong B' JJ' B J). apply segment_construction_3. assumption. assumption. ex_and H24 JJ'. assert(~Col A' B' J'). intro. apply H20. eapply col_conga_col. apply H26. apply conga_sym. assumption. assert(A' <> JJ'). intro. subst JJ'. apply H20. eapply col_conga_col. apply out_col in H24. apply col_permutation_2. apply H24. apply conga_sym. assumption. assert(B' <> JJ'). unfold Out in H24. spliter. auto. assert(~Col A' B' JJ'). intro. apply H26. apply col_permutation_2. eapply (col_transitivity_1 _ JJ'). assumption. apply col_permutation_5. apply out_col. assumption. apply col_permutation_1. assumption. assert(CongA A B C AA' B' CC'). eapply l11_10. apply H. apply out_trivial. auto. apply out_trivial. auto. apply l6_6. assumption. apply l6_6. assumption. assert(CongA A' B' J' A' B' JJ'). apply out2__conga. apply out_trivial. auto. apply l6_6. assumption. assert(Out B' I' JJ' \/ TS A' B' I' JJ'). apply conga_cop__or_out_ts. apply coplanar_perm_2, col_cop__cop with J'; Col; Cop. eapply conga_trans. apply conga_sym. apply H0. apply conga_sym. eapply conga_trans. apply conga_sym. apply H31. eapply conga_trans. apply conga_sym. apply H21. eapply l11_10. apply (conga_refl A B I). assumption. assumption. apply out_trivial. auto. assumption. apply out_trivial. auto. apply out_trivial. auto. induction H32. assert(CongA J B C J' B' C'). apply (l11_22b _ _ _ A _ _ _ A'). split. apply invert_one_side. apply in_angle_one_side. assumption. intro. apply H10. apply col_permutation_2. eapply (col_transitivity_1 _ J). assumption. apply out_col. assumption. apply col_permutation_5. assumption. eapply l11_25. apply HH. apply out_trivial. auto. apply out_trivial. auto. assumption. split. apply one_side_transitivity with I'; apply invert_one_side; assumption. split. apply conga_comm. assumption. assumption. assert(Cong A C AA' CC'). eapply cong2_conga_cong. eapply l11_10. apply H. apply out_trivial. auto. apply out_trivial. auto. apply l6_6. assumption. apply l6_6. assumption. apply cong_symmetry. apply cong_commutativity. assumption. apply cong_symmetry. assumption. assert(Cong A J AA' JJ'). eapply cong2_conga_cong. eapply l11_10. apply H0. apply out_trivial. auto. assumption. apply l6_6. assumption. apply l6_6. assumption. apply cong_symmetry. apply cong_commutativity. assumption. apply cong_symmetry. assumption. assert(CongA J' B' C' JJ' B' CC'). apply out2__conga; apply l6_6; assumption. assert(Cong J C JJ' CC'). eapply (cong2_conga_cong). eapply conga_trans. apply H33. apply H36. apply cong_symmetry. apply cong_commutativity. assumption. apply cong_symmetry. assumption. assert(Bet AA' JJ' CC'). apply (l4_6 A J C). apply H17. repeat split; assumption. apply l11_25 with JJ' AA' CC'; trivial. repeat split; auto. unfold Out in H11. spliter. auto. unfold Out in H12. spliter. auto. exists JJ'. split. assumption. right. apply out_trivial. auto. assert(OS B' A' I' JJ'). eapply out_out_one_side. apply invert_one_side. apply one_side_symmetry. apply H22. assumption. apply invert_two_sides in H32. apply l9_9 in H32. contradiction. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2