proposition: Lemma is_ang_conga_is_ang : forall A B C A' B' C' a, Ang A B C a -> CongA A B C A' B' C' -> Ang A' B' C' a.
proof: Proof. intros. unfold Ang in *. spliter. split. auto. 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