proposition: Lemma lcos_uniqueness : forall l a l1 l2, Lcos l1 l a-> Lcos l2 l a -> EqL l1 l2.
proof: Proof. intros. unfold Lcos in *. spliter. ex_and H6 A1. ex_and H7 B1. ex_and H6 C1. ex_and H3 A2. ex_and H10 B2. ex_and H3 C2. assert(Cong A1 C1 A2 C2). apply (lg_cong l); auto. assert(CongA B1 A1 C1 B2 A2 C2). apply (anga_conga a); auto. induction(eq_dec_points C1 B1). subst C1. assert(EqL l l1). apply ex_eqL; auto. exists A1. exists B1. split; auto. assert(Out A2 B2 C2). apply (l11_21_a B1 A1 B1). apply out_trivial. intro. subst B1. apply conga_distinct in H14. tauto. auto. assert(C2 = B2 \/ A2 = B2). apply(l8_9 C2 B2 A2). auto. apply out_col in H16. Col. induction H17. subst C2. assert(EqL l l2). apply ex_eqL; auto. exists A2. exists B2. split; auto. transitivity l; auto. symmetry; auto. subst B2. apply conga_distinct in H14. tauto. apply conga_distinct in H14. spliter. assert(CongA C1 B1 A1 C2 B2 A2). apply l11_16; auto. intro. subst C2. assert(Out A1 B1 C1). apply (l11_21_a B2 A2 B2). apply out_trivial; auto. apply conga_sym. auto. assert(C1 = B1 \/ A1 = B1). apply(l8_9 C1 B1 A1 ); auto. apply out_col in H20. Col. induction H21. subst C1. tauto. subst B1. tauto. assert( Cong C1 B1 C2 B2 /\ Cong A1 B1 A2 B2 /\ CongA B1 C1 A1 B2 C2 A2). apply(l11_50_2 C1 A1 B1 C2 A2 B2). intro. assert(C1 = B1 \/ A1 = B1). apply(l8_9 C1 B1 A1 ); auto. Col. induction H22. contradiction. subst B1. tauto. apply conga_comm. auto. apply conga_comm. auto. Cong. spliter. apply ex_eqL; auto. exists A1. exists B1. split; auto. apply (lg_cong_lg l2 A2 B2); auto. Cong. Qed.
imports: GeoCoq.Tarski_dev.Ch13_3_angles Morphisms