proposition: Lemma is_anga_conga_is_anga : forall A B C A' B' C' a, Ang_Acute A B C a -> CongA A B C A' B' C' -> Ang_Acute A' B' C' a.
proof: Proof. intros. unfold Ang_Acute in *. spliter. split. auto. apply anga_is_ang in H. unfold Q_CongA in H. ex_and H A0. ex_and H2 B0. ex_and H C0. assert(HH:= H3 A B C). destruct HH. assert(HH1:= H3 A' B' C'). destruct HH1. apply H5 in H1. apply H6. eapply conga_trans. apply H1. auto. Qed.
imports: GeoCoq.Tarski_dev.Ch13_2_length Setoid