proposition: Lemma lcos3_eq_trans : forall l1 a b c l2 d e f l3 g h i, Eq_Lcos3 l1 a b c l2 d e f -> Eq_Lcos3 l2 d e f l3 g h i -> Eq_Lcos3 l1 a b c l3 g h i.
proof: Proof. intros. unfold Eq_Lcos3 in *. ex_and H lp. ex_and H0 lq. exists lp. split; auto. assert(EqL lp lq). eapply (lcos3_uniqueness l2 _ _ d e f); auto. apply lcos3_lg_anga in H2. apply lcos3_lg_anga in H1. spliter. eapply (lcos3_eql_lcos3 l3 _ lq); auto. reflexivity. symmetry; auto. Qed.
imports: GeoCoq.Tarski_dev.Ch13_3_angles Morphisms