proposition: Lemma is_anga_to_is_ang : forall A B C a, Ang_Acute A B C a -> Ang A B C a.
proof: Proof. intros. unfold Ang_Acute in H. unfold Ang. spliter. split. apply anga_is_ang. auto. auto. Qed.
imports: GeoCoq.Tarski_dev.Ch13_2_length Setoid