proposition: Lemma ex_points_anga : forall a , Q_CongA_Acute a -> exists A, exists B, exists C, a A B C.
proof: Proof. intros. assert(HH:=H). apply anga_is_ang in H. ang_instance a A B C. exists A. exists B. exists C. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch13_2_length