proposition: Lemma lcos2_eq_trans : forall l1 a b l2 c d l3 e f, Eq_Lcos2 l1 a b l2 c d -> Eq_Lcos2 l2 c d l3 e f -> Eq_Lcos2 l1 a b l3 e f.
proof: Proof. intros. unfold Eq_Lcos2 in *. ex_and H lp. ex_and H0 lq. exists lp. split; auto. assert(EqL lp lq). eapply (lcos2_uniqueness l2 _ _ c d); auto. apply lcos2_lg_anga in H2. apply lcos2_lg_anga in H1. spliter. eapply (lcos2_eql_lcos2 l3 _ lq); auto. reflexivity. symmetry; auto. Qed.
imports: GeoCoq.Tarski_dev.Ch13_3_angles Morphisms