proposition: Lemma out546_suma__conga : forall A B C D E F G H I, SumA A B C D E F G H I -> Out E D F -> CongA A B C G H I.
proof: Proof. intros A B C D E F G H I Hsuma Hout. assert(A<>B/\B<>C/\D<>E/\E<>F/\G<>H/\H<>I) by (apply suma_distincts; auto). spliter. apply (suma2__conga A B C D E F A B C); auto. exists C. split. apply l11_21_b; try (apply out_trivial); auto. split. apply col124__nos; Col. split; Cop; CongA. Qed.
imports: GeoCoq.Tarski_dev.Ch11_angles