proposition: Lemma anga_col_null : forall a A B C, Q_CongA_Acute a -> a A B C -> Col A B C -> Out B A C /\ Q_CongA_Null_Acute a.
proof: Proof. intros. assert(HH:= anga_distincts a A B C H H0). spliter. assert(Out B A C). induction H1. assert(HP:=anga_acute a A B C H H0). assert(HH:=acute_not_bet A B C HP). contradiction. induction H1. unfold Out. repeat split; auto. unfold Out. repeat split; auto. left. Between. split. auto. apply (out_null_anga a A B C); auto. Qed.
imports: GeoCoq.Tarski_dev.Ch13_2_length Setoid