proposition: Lemma lcos_const_a : forall lp l a B, Lcos lp l a -> exists A, exists C, l A B /\ lp B C /\ a A B C.
proof: Proof. intros. assert(HH:=H). unfold Lcos in HH. spliter. clear H3. assert(HH:= ex_point_lg l B H1). ex_and HH A. assert(l A B). apply lg_sym; auto. exists A. assert(HH:= lcos_lg_not_null lp l a H). spliter. assert(A <> B). intro. subst A. apply H6. unfold Q_Cong_Null. split. auto. exists B. auto. assert(HH:= anga_const a A B H2 H7). ex_and HH C'. assert(HH:= anga_distincts a A B C' H2 H8). spliter. assert(B <> C'); auto. assert(HH:= ex_point_lg_out lp B C' H11 H0 H5). 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