proposition: Lemma lcos2_exists : forall l a b, Q_Cong l -> ~ Q_Cong_Null l -> Q_CongA_Acute a -> Q_CongA_Acute b -> exists lp, Lcos2 lp l a b.
proof: Proof. intros. assert(HH:= lcos_exists l a H1 H H0). ex_and HH la. apply lcos_lg_anga in H3. spliter. assert(~ Q_Cong_Null la /\ ~ Q_Cong_Null l). apply (lcos_lg_not_null _ _ a). auto. spliter. clear H8. assert(HH:= lcos_exists la b H2 H5 H7). ex_and HH lab. exists lab. unfold Lcos2. exists la. split; auto. Qed.
imports: GeoCoq.Tarski_dev.Ch13_3_angles Morphisms