proposition: Lemma lcos_const0 : forall l lp a, Lcos lp l a -> Q_CongA_Null_Acute a -> exists A, exists B, exists C, l A B /\ lp B C /\ a A B C.
proof: Proof. intros. assert(HH:=H). unfold Lcos in HH. spliter. ex_and H4 A. ex_and H5 B. ex_and H4 C. exists C. exists A. exists B. repeat split. apply lg_sym; auto. auto. apply anga_sym; auto. Qed.
imports: GeoCoq.Tarski_dev.Ch13_3_angles Morphisms