proposition: Lemma lcos_const : forall lp l a, Lcos lp l a -> exists A, exists B, exists C, lp A B /\ l B C /\ a A B C.
proof: Proof. intros. unfold Lcos in H. spliter. ex_and H2 A. ex_and H3 B. ex_and H2 C. exists B. exists A. exists C. repeat split; auto. apply lg_sym; auto. Qed.
imports: GeoCoq.Tarski_dev.Ch13_3_angles Morphisms