proposition: Lemma lcos_const1 : forall l lp a P, Lcos lp l a -> ~ Q_CongA_Null_Acute a -> exists A, exists B, exists C, ~Col A B P /\ OS A B C P /\ l A B /\ lp B C /\ a A B C.
proof: Proof. intros. assert(HH:=H). unfold Lcos in HH. spliter. assert(HH:= (lcos_lg_not_null lp l a H)). spliter. lg_instance_not_col l P A B. exists A. exists B. assert(HH:=anga_const_o a A B P H8 H0 H3). ex_and HH C'. assert(A <> B /\ B <> C'). assert(HP:= anga_distinct a A B C' H3 H9). spliter. auto. spliter. assert(HH:=ex_point_lg_out lp B C' H12 H1 H5). ex_and HH C. exists C. repeat split; auto. assert(~ Col A B C'). unfold OS in H10. ex_and H10 D. unfold TS in H10. spliter. intro. apply H10. Col. assert(HP:=out_one_side_1 A B C' C B H15). eapply (one_side_transitivity _ _ _ C'). apply one_side_symmetry. apply HP. Col. apply l6_6. auto. auto. apply (anga_out_anga a A B C'); auto. apply out_trivial. auto. apply l6_6. auto. Qed.
imports: GeoCoq.Tarski_dev.Ch13_3_angles Morphisms