proposition: Lemma lea_trans : forall A B C A1 B1 C1 A2 B2 C2, LeA A B C A1 B1 C1 -> LeA A1 B1 C1 A2 B2 C2 -> LeA A B C A2 B2 C2.
proof: Proof. intros. assert(Hlea1 := H). assert (Hlea2 := H0). unfold LeA in H. unfold LeA in H0. ex_and H P1. ex_and H0 P2. assert( A <> B /\ C <> B /\ A1 <> B1 /\ C1 <> B1 /\ A2 <> B2 /\ C2 <> B2). unfold CongA in *. unfold InAngle in H0. spliter. repeat split; assumption. spliter. assert(HH1 := or_bet_out A B C). induction HH1. assert(Bet A1 B1 P1). eapply bet_conga__bet. apply H9. assumption. assert(Bet A1 B1 C1). eapply bet_in_angle_bet. apply H10. assumption. assert(Bet A2 B2 P2). eapply bet_conga__bet. apply H11. assumption. assert(Bet A2 B2 C2). eapply bet_in_angle_bet. apply H12. assumption. apply l11_31_2; assumption. induction H9. apply l11_31_1; assumption. assert(HH2 := or_bet_out A2 B2 C2). induction HH2. apply l11_31_2; assumption. induction H10. assert(Out B2 A2 P2). eapply in_angle_out. apply H10. assumption. assert(Out B1 A1 C1). eapply l11_21_a. apply H11. apply conga_sym. assumption. assert(Out B1 A1 P1). eapply in_angle_out. apply H12. assumption. assert(Out B A C). eapply l11_21_a. apply H13. apply conga_sym. assumption. apply l11_31_1; assumption. assert(exists P, CongA A B C A2 B2 P /\ OS A2 B2 P C2). apply angle_construction_1; assumption. ex_and H11 P. assert (OS A2 B2 P2 C2). apply in_angle_one_side. assumption. assert (B2 <> A2). auto. assert(P2 <> A2). intro. subst P2. assert(Out B1 A1 C1). apply (l11_21_a A2 B2 A2). apply out_trivial. auto. apply conga_sym. apply H2. assert(Out B1 A1 P1). eapply in_angle_out. apply H14. assumption. assert(Out B A C). eapply l11_21_a. apply H15. apply conga_sym. assumption. apply H9. apply out_col in H16. apply col_permutation_4. assumption. assert(HH:=or_bet_out A2 B2 P2 ). induction HH. assert (Bet A2 B2 C2). eapply bet_in_angle_bet. apply H15. apply H0. intro. apply H10. unfold Col. left. assumption. induction H15. assert(Out B1 A1 C1). eapply l11_21_a. apply H15. apply conga_sym. assumption. assert( Out B1 A1 P1). eapply in_angle_out. apply H16. assumption. assert (Out B A C). eapply l11_21_a. apply H17. apply conga_sym. assumption. apply False_ind. apply H9. apply out_col in H18. apply col_permutation_4. assumption. intro. apply H15. apply col_permutation_4. assumption. assumption. unfold CongA in H2. assert(OS A2 B2 P P2). eapply one_side_transitivity. apply H12; eapply l11_21_a. apply one_side_symmetry. assumption. unfold LeA. exists P. split. eapply (in_angle_trans _ _ _ P2). apply (conga_preserves_in_angle A1 B1 C1 P1); trivial. eapply conga_trans. apply conga_sym. apply H1. assumption. assumption. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2