proposition: Lemma lcos2_uniqueness: forall l l1 l2 a b, Lcos2 l1 l a b -> Lcos2 l2 l a b -> EqL l1 l2.
proof: Proof. intros. unfold Lcos2 in *. ex_and H la. ex_and H0 lb. assert(EqL la lb). apply (l13_6 a _ _ l); auto. apply lcos_lg_anga in H2. apply lcos_lg_anga in H1. spliter. assert(Lcos l2 la b). rewrite H3;auto. apply (l13_6 b _ _ la); auto. Qed.
imports: GeoCoq.Tarski_dev.Ch13_3_angles Morphisms