proposition: Lemma anga_conga_anga : forall a A B C A' B' C' , Q_CongA_Acute a -> a A B C -> CongA A B C A' B' C' -> a A' B' C'.
proof: Proof. intros. unfold Q_CongA_Acute in H. ex_and H A0. ex_and H2 B0. ex_and H C0. assert(HH := H2 A B C). assert(HP := H2 A' B' C'). destruct HH. destruct HP. apply H4 in H0. assert(CongA A0 B0 C0 A' B' C'). eapply conga_trans. apply H0. apply H1. apply H5. auto. Qed.
imports: GeoCoq.Tarski_dev.Ch13_2_length Setoid