proposition: Lemma lcos_not_lg_null : forall lp l a, Lcos lp l a -> ~ Q_Cong_Null lp.
proof: Proof. intros. intro. unfold Q_Cong_Null in H0. spliter. unfold Lcos in H. spliter. ex_and H4 B. ex_and H5 A. ex_and H4 C. ex_and H1 P. unfold Q_Cong in H0. ex_and H0 X. ex_and H1 Y. assert(HH:= (H0 B A)). destruct HH. assert(HH:= (H0 P P)). destruct HH. apply H11 in H8. apply H9 in H5. assert(Cong B A P P). apply (cong_transitivity _ _ X Y); Cong. assert(A = B). eapply (cong_identity _ _ P). Cong. assert(HH:=anga_distincts a A B C H3 H7). spliter. contradiction. Qed.
imports: GeoCoq.Tarski_dev.Ch13_3_angles Morphisms