proposition: Lemma anga_const_o : forall a A B P, ~Col A B P -> ~ Q_CongA_Null_Acute a -> Q_CongA_Acute a -> exists C, a A B C /\ OS A B C P.
proof: Proof. intros. assert(Q_CongA a). apply anga_is_ang; auto. assert(Q_CongA_nNull a). unfold Q_CongA_nNull. split. auto. intros A' B' C' HP. intro. apply H0. eapply (out_null_anga a A' B' C'); auto. assert(Q_CongA_nFlat a). apply anga_not_flat. auto. assert(HH:= ang_const_o a A B P H H2 H3 H4). auto. Qed.
imports: GeoCoq.Tarski_dev.Ch13_2_length Setoid