proposition: Lemma anga_not_null_lg : forall a l A B C, Q_CongA_Acute a -> Q_Cong l -> a A B C -> l A B -> ~ Q_Cong_Null l.
proof: Proof. intros. intro. unfold Q_CongA_Acute in H. unfold Q_Cong_Null in H3. spliter. unfold Q_Cong in H0. ex_and H A0. ex_and H5 B0. ex_and H C0. assert(HH:= H5 A B C). destruct HH. assert(CongA A0 B0 C0 A B C). apply H7. auto. apply conga_distinct in H8. spliter. ex_and H0 A1. ex_and H13 B1. assert(HH:= H0 A B). destruct HH. ex_and H4 A'. assert(HH:= H0 A' A'). destruct HH. assert(Cong A1 B1 A' A'). apply H16. auto. assert(Cong A1 B1 A B). apply H14. auto. apply cong_identity in H17. subst B1. apply cong_symmetry in H18. apply cong_identity in H18. contradiction. Qed.
imports: GeoCoq.Tarski_dev.Ch13_2_length Setoid