proposition: Lemma lcos_exists : forall l a, Q_CongA_Acute a -> Q_Cong l -> ~ Q_Cong_Null l -> exists lp, Lcos lp l a.
proof: Proof. intros. lg_instance l A B. induction(is_null_anga_dec a). exists l. apply null_lcos; auto. anga_instance1 a A B C. assert(~ Col B C A). intro. assert(Out B A C /\ Q_CongA_Null_Acute a). apply(anga_col_null a A B C H H4). Col. apply H3. tauto. assert(HH:= l8_18_existence B C A H5). ex_and HH P. assert(HH:=lg_exists B P). ex_and HH lp. exists lp. assert(Acute A B C). unfold Q_CongA_Acute in H. ex_and H A'. ex_and H10 B'. ex_and H C'. assert(HH:=H10 A B C). destruct HH. assert(HP:= H12 H4). apply (acute_lea_acute _ _ _ A' B' C'); auto. unfold LeA. exists C'. split. apply conga_distinct in HP. spliter. apply inangle3123; auto. apply conga_sym. auto. unfold Lcos. repeat split; auto. exists B. exists P. exists A. repeat split; auto. apply perp_in_per. apply perp_in_comm. apply perp_perp_in. apply perp_sym. apply (perp_col _ C). intro. subst P. assert(Per A B C). apply perp_in_per. apply perp_in_comm. apply perp_perp_in. Perp. apply acute_not_per in H10. contradiction. Perp. Col. apply (lg_sym l); auto. assert(HH:=H10). unfold Acute in HH. apply(anga_sym a); auto. apply(anga_out_anga a A B C A P); auto. apply out_trivial. intro. subst B. apply H5. Col. eapply (perp_acute_out _ _ A). apply acute_sym. auto. Perp. Col. intro. apply H1. unfold Q_Cong_Null. split; auto. subst B. exists A. auto. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch13_3_angles Morphisms