proposition: Lemma lcos_const_cb : forall lp l a B C, Lcos lp l a -> lp B C -> exists A, l A B /\ a A B C.
proof: Proof. intros. assert(HH:=H). unfold Lcos in HH. spliter. clear H4. assert(HH:= lcos_lg_not_null lp l a H). spliter. assert(C <> B). intro. subst C. apply H4. unfold Q_Cong_Null. split. auto. exists B. auto. assert(HH:= anga_const a C B H3 H6). ex_and HH A'. assert(HH:= anga_distincts a C B A' H3 H7). spliter. assert(B <> A'); auto. assert(HH:= ex_point_lg_out l B A' H10 H2 H5). ex_and HH A. exists A. split. apply lg_sym; auto. apply(anga_out_anga a A' B C); auto. apply anga_sym; auto. apply l6_6. auto. apply out_trivial. auto. Qed.
imports: GeoCoq.Tarski_dev.Ch13_3_angles Morphisms