proposition: Lemma all_eqaa : forall A B C a1 a2, Ang_Acute A B C a1 -> Ang_Acute A B C a2 -> EqA a1 a2.
proof: Proof. intros. apply ex_eqaa. exists A. exists B. exists C. split; auto. Qed.
imports: GeoCoq.Tarski_dev.Ch13_2_length Setoid