proposition: Lemma out213_suma__conga : forall A B C D E F G H I, SumA A B C D E F G H I -> Out B A C -> CongA D E F G H I.
proof: Proof. intros A B C D E F G H I Hsuma Hout. apply (out546_suma__conga D E F A B C); auto. apply suma_sym; auto. Qed.
imports: GeoCoq.Tarski_dev.Ch11_angles