proposition: Lemma ang_conga : forall a A B C A' B' C', Q_CongA a -> a A B C -> a A' B' C' -> CongA A B C A' B' C'.
proof: Proof. intros. unfold Q_CongA in H. ex_and H A0. ex_and H2 B0. ex_and H C0. assert(HH:=H3 A B C). assert(HH1:= H3 A' B' C'). destruct HH. destruct HH1. apply H5 in H0. apply H7 in H1. eapply conga_trans. apply conga_sym. apply H0. auto. Qed.
imports: GeoCoq.Tarski_dev.Ch13_2_length