proposition: Lemma l11_29_b : forall A B C D E F, (exists Q, InAngle C A B Q /\ CongA A B Q D E F) -> LeA A B C D E F.
proof: Proof. intros. ex_and H Q. unfold LeA. assert(HH:=H). unfold InAngle in HH. spliter. ex_and H4 X. induction H5. subst X. assert(exists P, CongA A B C D E P). apply angle_construction_3. assumption. assumption. unfold CongA in H0. spliter. assumption. ex_and H5 P. exists P. split. assert(Bet D E F). eapply bet_conga__bet. apply H4. assumption. apply in_angle_line. unfold CongA in H6. spliter. assumption. unfold CongA in H6. spliter. assumption. unfold CongA in H0. spliter. assumption. assumption. assumption. assert(exists DD, Out E D DD /\ Cong E DD B A). apply segment_construction_3. unfold CongA in H0. spliter. auto. auto. ex_and H6 DD. assert(exists FF, Out E F FF /\ Cong E FF B Q). apply segment_construction_3. unfold CongA in H0. spliter. auto. auto. ex_and H8 FF. assert(D <> E /\ DD <> E /\ F <> E /\ FF <> E). unfold Out in *. spliter. repeat split; try assumption. spliter. assert(HI:=or_bet_out A B C). induction HI. exists F. split. apply inangle3123. assumption. assumption. assert(CongA A B C A B Q). apply out2__conga. apply out_trivial. auto. unfold Out in H5. spliter. induction H16. assert(Bet A B X). eapply between_inner_transitivity. apply H14. assumption. assert(Bet B X Q). eapply between_exchange3. apply H17. assumption. assert(Bet B Q C \/ Bet B C Q). apply l5_1 with X; auto. unfold Out. repeat split; auto. assert(Bet A B X). eapply outer_transitivity_between. apply H14. assumption. auto. assert(Bet B X Q). eapply between_exchange3. apply H17. assumption. assert(Bet B C Q). eapply between_exchange4. apply H16. assumption. unfold Out. repeat split. auto. auto. right. assumption. eapply conga_trans. apply H15. assumption. induction H14. exists D. split. apply inangle1123. assumption. assumption. assert(CongA A B C A B A). apply out2__conga. apply out_trivial. auto. assumption. eapply conga_trans. apply H15. apply conga_trivial_1. assumption. assumption. assert(HJ:=or_bet_out A B Q). induction HJ. assert(exists P, CongA A B C D E P). apply angle_construction_3. auto. auto. unfold Out in H6. spliter. auto. ex_and H16 P. exists P. split. apply in_angle_line. unfold CongA in H17. spliter. assumption. assumption. assumption. eapply bet_conga__bet. apply H15. assumption. assumption. induction H15. assert(Out B A C). eapply in_angle_out. apply H15. assumption. apply False_ind. apply H14. unfold Out in H16. spliter. unfold Col. induction H18. right; right. apply between_symmetry. assumption. right; left. assumption. assert(exists P, CongA A B C D E P /\ OS D E P F). eapply angle_construction_1. assumption. eapply ncol_conga_ncol. apply H15. apply H0. ex_and H16 P. exists P. split. assert(exists PP, Out E P PP /\ Cong E PP B X). eapply segment_construction_3. unfold CongA in H16. spliter. auto. unfold Out in H5. spliter. auto. ex_and H18 PP. apply l11_25 with PP DD FF; trivial. repeat split. auto. auto. unfold Out in H18. spliter. auto. exists PP. split. assert(CongA C B Q P E F). apply l11_22b with A D. split. apply invert_one_side. eapply in_angle_one_side. assumption. intro. apply H14. apply col_permutation_4. assumption. assumption. split. apply invert_one_side. apply H17. split. apply conga_comm. assumption. assumption. assert (Cong DD FF A Q). eapply cong2_conga_cong. eapply l11_10. apply conga_sym. apply H0. apply l6_6. assumption. apply l6_6. assumption. apply l6_6. apply out_trivial. auto. apply out_trivial. auto. apply cong_commutativity. assumption. assumption. assert(Cong A X DD PP). eapply cong2_conga_cong. eapply l11_10. apply H16. 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(Cong X Q PP FF). eapply cong2_conga_cong. eapply l11_10. apply H20. assumption. apply out_trivial. auto. apply l6_6. assumption. apply l6_6. assumption. apply cong_symmetry. apply cong_commutativity. assumption. apply cong_symmetry. assumption. eapply l4_6. apply H4. repeat split. assumption. apply cong_symmetry. assumption. assumption. right. apply out_trivial. unfold Out in H15. spliter. unfold Out in H18. spliter. auto. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2