proposition: Lemma not_null_not_col : forall a A B C, Q_CongA_Acute a -> ~ Q_CongA_Null_Acute a -> a A B C -> ~Col A B C.
proof: Proof. intros. intro. apply H0. unfold Q_CongA_Null_Acute. split. auto. assert(Acute A B C). apply (anga_acute a); auto. intros. assert(Out B A C). apply acute_col__out; auto. assert(HH:= anga_conga a A B C A0 B0 C0 H H1 H4). apply (l11_21_a A B C); auto. Qed.
imports: GeoCoq.Tarski_dev.Ch13_2_length Setoid