proposition: Lemma out_out_anga : forall a A B C A' B' C', Q_CongA_Acute a -> Out B A C -> Out B' A' C' -> a A B C -> a A' B' C'.
proof: Proof. intros. assert(CongA A B C A' B' C'). apply l11_21_b; auto. apply (anga_conga_anga a A B C); auto. Qed.
imports: GeoCoq.Tarski_dev.Ch13_2_length Setoid