proposition: Lemma l13_7 : forall a b l la lb lab lba, Lcos la l a -> Lcos lb l b -> Lcos lab la b -> Lcos lba lb a -> EqL lab lba.
proof: Proof. intros. apply lcos_lg_anga in H. apply lcos_lg_anga in H0. apply lcos_lg_anga in H1. apply lcos_lg_anga in H2. spliter. clean_duplicated_hyps. induction (is_null_anga_dec a). assert(HH:=null_lcos_eql lba lb a H2 H3). assert(HP:=null_lcos_eql la l a H H3). assert(Lcos lab l b) by (rewrite HP;assumption). assert(HQ:= l13_6 b lb lab l H0 H5). rewrite <- HQ;assumption. induction (is_null_anga_dec b). assert(HH:=null_lcos_eql lab la b H1 H5). assert(HP:=null_lcos_eql lb l b H0 H5). assert(Lcos lba l a) by (rewrite HP;auto). assert(HQ:= l13_6 a la lba l H H6). rewrite HH in HQ;assumption. assert(HH:=lcos_const la l a H). ex_and HH C. ex_and H6 A. ex_and H8 B. assert(HH:= anga_distincts a C A B H14 H9). spliter. assert(~Col A B C). intro. apply H3. assert(Col C A B). Col. assert(HH:= anga_col_null a C A B H14 H9 H18). spliter. auto. assert(HH:=l10_2_existence B A C). ex_and HH P. assert( ~ Col B A P). eapply (osym_not_col _ _ C). apply l10_4. auto. intro. apply H17. Col. assert(l B A). apply lg_sym; auto. assert(HH:= lcos_const_o lb l b B A P H19 H5 H12 H10 H11 H20 H0). ex_and HH D. assert(TS B A P C). apply l10_14. intro. subst P. assert(Col C B A). apply(l10_8 B A C); auto. apply H19. Col. auto. auto. assert(TS B A D C). eapply (l9_8_2 _ _ P). auto. apply one_side_symmetry. auto. assert(Per A C B). apply (lcos_per _ _ _ la l a); auto. apply lg_sym; auto. assert(Per A D B). apply (lcos_per _ _ _ lb l b); auto. apply anga_sym; auto. assert(~ Col C D A). intro. assert(Per B C D). apply(per_col B C A D); auto. apply l8_2. auto. Col. assert(Per B D C). apply(per_col B D A C); auto. unfold OS in H21. ex_and H21 T. unfold TS in H21. spliter. intro. subst D. apply H21. Col. apply l8_2. auto. Col. assert(C = D). apply (l8_7 B); auto. subst D. unfold TS in H25. spliter. ex_and H32 T. assert(C=T). apply between_identity. auto. subst T. contradiction. assert(HH:= l8_18_existence C D A H28). ex_and HH E. assert(CongA B A C D A E /\ CongA B A D C A E /\ Bet C E D). apply(l13_2 A B C D E). apply invert_two_sides. apply l9_2. auto. apply l8_2. auto. apply l8_2. auto. auto. apply perp_sym. auto. spliter. assert(a D A E). eapply (anga_conga_anga a B A C); auto. apply anga_sym; auto. assert(b C A E). eapply (anga_conga_anga b B A D); auto. assert(Perp C E A E). eapply (perp_col _ D) . intro. subst E. apply H5. unfold Q_CongA_Null_Acute. split; auto. intros. assert(CongA A0 B0 C0 C A C). apply (anga_conga b); auto. apply (l11_21_a C A C A0 B0 C0 ). apply out_trivial; auto. apply conga_sym. auto. auto. auto. assert(lab A E). apply (lcos_lg b lab la A E C H1). apply perp_sym in H36. apply perp_right_comm in H36. auto. apply anga_sym; auto. apply lg_sym; auto. assert(Perp D E A E). eapply (perp_col _ C) . intro. subst E. apply H3. unfold Q_CongA_Null_Acute. split; auto. intros. assert(CongA A0 B0 C0 D A D). apply (anga_conga a); auto. apply (l11_21_a D A D A0 B0 C0 ). apply out_trivial; auto. apply perp_not_eq_2 in H36. auto. apply conga_sym. auto. Perp. Col. assert(lba A E). apply (lcos_lg a lba lb A E D). auto. Perp. auto. apply anga_sym; auto. auto. apply ex_eql. exists A. exists E. split. unfold Len. split; auto. unfold Len. split; auto. assumption. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch13_3_angles Morphisms