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