proposition: Lemma anga_col_out : forall a A B C, Q_CongA_Acute a -> a A B C -> Col A B C -> Out B A C.
proof: Proof. intros. assert(Acute A B C). apply (anga_acute a); auto. unfold Col in H1. induction H1. apply acute_not_bet in H2. contradiction. unfold Out. apply (anga_distinct a A B C) in H. spliter. repeat split; auto. induction H1. right. auto. left. Between. auto. Qed.
imports: GeoCoq.Tarski_dev.Ch13_2_length Setoid