proposition: Lemma lcos3_lcos_1_2 : forall lp l a b c, Lcos3 lp l a b c <-> exists la, Lcos la l a /\ Lcos2 lp la b c.
proof: Proof. intros. split. intro. unfold Lcos3 in H. ex_and H la. ex_and H0 lab. exists la. split; auto. unfold Lcos2. exists lab. split; auto. intro. ex_and H la. unfold Lcos2 in H0. ex_and H0 lab. unfold Lcos3. exists la. exists lab. apply lcos_lg_anga in H0. apply lcos_lg_anga in H1. spliter. split; auto. Qed.
imports: GeoCoq.Tarski_dev.Ch13_3_angles Morphisms