proposition: Lemma lea_asym : forall A B C D E F, LeA A B C D E F -> LeA D E F A B C -> CongA A B C D E F.
proof: Proof. intros. induction (col_dec A B C). induction (bet_dec A B C). apply lea_distincts in H0; spliter. apply conga_line; auto. ex_and H P. apply bet_in_angle_bet with P; trivial. apply (bet_conga__bet A B C); assumption. apply not_bet_out in H2; trivial. apply l11_21_b; trivial. ex_and H0 P. apply (l11_21_a A B P). apply in_angle_out with C; assumption. apply conga_sym; assumption. apply l11_29_a in H. unfold LeA in *. ex_and H Q. ex_and H0 P. assert(A <> B /\ Q <> B /\ P <> B /\ D <> E /\ F <> E). unfold CongA in *. spliter. repeat split; assumption. spliter. assert(CongA A B Q A B P). eapply conga_trans. apply H2. assumption. assert(HH1:= or_bet_out A B Q). induction HH1. assert(Bet A B P). eapply bet_conga__bet. apply H10. assumption. assert(Bet A B C). eapply bet_in_angle_bet. apply H11. assumption. assert(Bet D E F). eapply bet_conga__bet. apply H10. assumption. eapply conga_line; try assumption. unfold InAngle in H0. spliter. auto. auto. induction H10. assert(Out E D F). eapply l11_21_a. apply H10. assumption. assert(Out B A P). eapply l11_21_a. apply H11. apply H3. assert(Out B A C). eapply in_angle_out. apply H10. assumption. eapply l11_21_b. assumption. assumption. assert(HH2:= or_bet_out A B P). induction HH2. assert(Bet A B C). eapply bet_in_angle_bet. apply H11. assumption. assert(Bet D E F). eapply bet_conga__bet. apply H11. apply conga_sym. assumption. apply conga_line; try assumption. unfold InAngle in H0. spliter. auto. auto. induction H11. assert(Out B A Q). eapply l11_21_a. apply H11. apply conga_sym. assumption. assert (Out B A C). eapply in_angle_out. apply H12. assumption. assert(Out E D F). eapply l11_21_a. apply H12. assumption. apply l11_21_b. assumption. assumption. assert(Out B P Q \/ TS A B P Q). apply conga_cop__or_out_ts. apply coplanar_trans_1 with C; Cop; Col. apply conga_sym. assumption. induction H12. assert(InAngle C A B P). eapply l11_25. apply H. apply out_trivial. auto. assumption. apply out_trivial. intro. subst C. unfold InAngle in H0. spliter. absurde. assert(CongA A B C A B P). apply in_angle_asym; assumption. eapply conga_trans. apply H14. eapply conga_trans. apply conga_sym. apply H9. assumption. assert(C <> B). unfold InAngle in H0. spliter. assumption. assert(HH:=or_bet_out A B C). induction HH. assert(Bet A B Q). eapply bet_in_angle_bet. apply H14. apply H. apply False_ind. apply H10. unfold Col. left. assumption. induction H14. assert(Out B A P). eapply in_angle_out. apply H14. assumption. apply False_ind. apply H11. apply out_col in H15. apply col_permutation_4. assumption. apply in_angle_one_side in H. apply in_angle_one_side in H0. assert(OS A B P Q). eapply one_side_transitivity. apply H0. assumption. apply l9_9 in H15. contradiction. assumption. assumption. intro. apply H11. apply col_permutation_4. assumption. assumption. intro. apply H14. apply col_permutation_4. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2