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