proposition: Lemma lcos_const_o : forall lp l a A B P, ~ Col A B P -> ~ Q_CongA_Null_Acute a -> Q_Cong l -> Q_Cong lp -> Q_CongA_Acute a -> l A B -> Lcos lp l a -> exists C, OS A B C P /\ a A B C /\ lp B C.
proof: Proof. intros. assert(HH:= anga_const_o a A B P H H0 H3). ex_and HH C'. assert(A <> B /\ C' <> B). apply (anga_distincts a); auto. spliter. assert(HH:= lcos_not_lg_null lp l a H5). assert (B <> C'). intro. apply H9. auto. assert(HP:=lg_exists C' B). ex_and HP lc'. assert(HQ:=anga_not_lg_null a l lc' A B C' H1 H11 H3 H4 H12 H6). spliter. assert(HR:= ex_point_lg_out lp B C' H10 H2 HH). ex_and HR C. exists C. split. apply invert_one_side. apply one_side_symmetry. apply (out_out_one_side _ _ _ C'). apply invert_one_side. apply one_side_symmetry. auto. apply l6_6. auto. split. eapply (anga_out_anga a A B C'); auto. apply out_trivial. auto. apply l6_6. auto. auto. Qed.
imports: GeoCoq.Tarski_dev.Ch13_3_angles Morphisms