proposition: Lemma l13_6 : forall a lc ld l, Lcos lc l a -> Lcos ld l a -> EqL lc ld.
proof: Proof. intros. unfold Lcos in *. spliter. ex_and H6 X1. ex_and H7 Y1. ex_and H6 Z1. ex_and H3 X2. ex_and H10 Y2. ex_and H3 Z2. clean_duplicated_hyps. assert(Len X1 Z1 l). split; auto. assert(Len X2 Z2 l). split; auto. assert(Cong X1 Z1 X2 Z2). eapply (is_len_cong _ _ _ _ l); auto. assert(Ang_Acute Y1 X1 Z1 a). split; auto. assert(Ang_Acute Y2 X2 Z2 a). split; auto. assert(CongA Y1 X1 Z1 Y2 X2 Z2). apply (is_anga_conga _ _ _ _ _ _ a); split; auto. assert(Len X1 Y1 lc). split; auto. assert(Len X2 Y2 ld). split; auto. induction(eq_dec_points Z1 Y1). subst Z1. assert(Out X2 Y2 Z2). apply (eq_conga_out Y1 X1); auto. assert(Y2 = Z2). assert(Z2 = Y2 \/ X2 = Y2). apply l8_9. auto. apply out_col in H19. Col. induction H20. auto. unfold Out in H19. spliter. subst Y2. tauto. subst Z2. assert(EqL l lc). apply ex_eql. exists X1. exists Y1. split; auto. assert(EqL l ld). apply ex_eql. exists X2. exists Y2. split; auto. transitivity l;auto. symmetry; auto. assert(Z2 <> Y2). intro. subst Z2. assert(Out X1 Y1 Z1). apply (eq_conga_out Y2 X2). apply conga_sym. auto. assert(Y1 = Z1). assert(Z1 = Y1 \/ X1 = Y1). apply l8_9. auto. apply out_col in H20. Col. induction H21. auto. subst Y1. unfold Out in H20. spliter. tauto. subst Z1. tauto. apply conga_distinct in H16. spliter. assert(CongA X1 Y1 Z1 X2 Y2 Z2). apply l11_16; Perp; auto. assert(~Col Z1 X1 Y1). intro. assert(X1 = Y1 \/ Z1 = Y1). apply l8_9. Perp. Col. induction H27. subst Y1. tauto. contradiction. apply conga_comm in H16. apply cong_commutativity in H13. assert(HH:=l11_50_2 Z1 X1 Y1 Z2 X2 Y2 H26 H25 H16 H13). spliter. apply ex_eql. exists X1. exists Y1. split. auto. eapply is_len_cong_is_len. apply H18. Cong. Qed.
imports: GeoCoq.Tarski_dev.Ch13_3_angles