proposition: Lemma lcos_const_ab : forall lp l a B A, Lcos lp l a -> l A B -> exists C, lp B C /\ 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(A <> B). intro. subst A. apply H5. unfold Q_Cong_Null. split. auto. exists B. auto. assert(HH:= anga_const a A B H3 H6). ex_and HH C'. assert(HH:= anga_distincts a A B C' H3 H7). spliter. assert(B <> C'); auto. assert(HH:= ex_point_lg_out lp B C' H10 H1 H4). ex_and HH C. exists C. repeat split; auto. apply (anga_out_anga a A B C' A C); auto. apply out_trivial. auto. apply l6_6. auto. Qed.
imports: GeoCoq.Tarski_dev.Ch13_3_angles Morphisms