proposition: Lemma lcos_eq_trans : forall la a lb b lc c, Eq_Lcos la a lb b -> Eq_Lcos lb b lc c -> Eq_Lcos la a lc c.
proof: Proof. intros. unfold Eq_Lcos in *. ex_and H lab. ex_and H0 lbc. assert(HH:= l13_6 b lab lbc lb H1 H0). assert(Lcos lbc la a). rewrite <- HH. apply lcos_lg_anga in H. tauto. exists lbc. split; auto. Qed.
imports: GeoCoq.Tarski_dev.Ch13_3_angles Morphisms