proposition: Lemma ex_eqaa : forall a1 a2, (exists A , exists B, exists C, Ang_Acute A B C a1 /\ Ang_Acute A B C a2) -> EqA a1 a2.
proof: Proof. intros. apply ex_eqa. ex_and H A. ex_and H0 B. ex_and H C. exists A. exists B. exists C. split; apply is_anga_to_is_ang; auto. Qed.
imports: GeoCoq.Tarski_dev.Ch13_2_length Setoid