proposition: Lemma lcos3_uniqueness: forall l l1 l2 a b c, Lcos3 l1 l a b c -> Lcos3 l2 l a b c -> EqL l1 l2.
proof: Proof. intros. unfold Lcos3 in *. ex_and H la. ex_and H1 lab. ex_and H0 la'. ex_and H3 lab'. assert(EqL la la'). apply (l13_6 a _ _ l); auto. apply lcos_lg_anga in H2. apply lcos_lg_anga in H3. apply lcos_lg_anga in H. apply lcos_lg_anga in H4. spliter. assert(Lcos lab' la b). rewrite H5;auto. assert(EqL lab lab') by (apply (l13_6 b _ _ la); auto). assert(Lcos l2 lab c). rewrite H19. auto. apply (l13_6 c _ _ lab); auto. Qed.
imports: GeoCoq.Tarski_dev.Ch13_3_angles Morphisms