proposition: Lemma lcos_eql_lcos : forall lp1 l1 lp2 l2 a, EqL lp1 lp2 -> EqL l1 l2 -> Lcos lp1 l1 a -> Lcos lp2 l2 a.
proof: Proof. intros. unfold Lcos in *. spliter. ex_and H4 A. ex_and H5 B. ex_and H4 C. assert(HH:=lg_eql_lg l1 l2 H2 H0). assert(HP:=lg_eql_lg lp1 lp2 H1 H). repeat split; auto. exists A. exists B. exists C. unfold EqL in *. spliter. repeat split; auto. apply H. auto. apply H0; auto. Qed.
imports: GeoCoq.Tarski_dev.Ch13_3_angles Morphisms