proposition: Lemma ex_eqa : forall a1 a2, (exists A , exists B, exists C, Ang A B C a1 /\ Ang A B C a2) -> EqA a1 a2.
proof: Proof. intros. ex_and H A. ex_and H0 B. ex_and H C. assert(HH:=H). assert(HH0:=H0). unfold Ang in HH. unfold Ang in HH0. spliter. unfold EqA. repeat split; auto; intro. assert(CongA A B C A0 B0 C0). eapply (is_ang_conga _ _ _ _ _ _ a1); auto. split; auto. assert(Ang A0 B0 C0 a2). apply (is_ang_conga_is_ang A B C); auto. unfold Ang in H7. tauto. assert(CongA A B C A0 B0 C0). eapply (is_ang_conga _ _ _ _ _ _ a2); auto. split; auto. assert(Ang A0 B0 C0 a1). apply (is_ang_conga_is_ang A B C); auto. unfold Ang in H7. tauto. Qed.
imports: GeoCoq.Tarski_dev.Ch13_2_length