proposition: Lemma out6_suma__suma : forall A B C D E F G H I A' C' D' F' G' I', SumA A B C D E F G H I -> Out B A A' -> Out B C C' -> Out E D D' -> Out E F F' -> Out H G G' -> Out H I I' -> SumA A' B C' D' E F' G' H I'.
proof: Proof. intros. assert_diffs. apply (conga3_suma__suma A B C D E F G H I); auto; apply conga_sym; apply out2__conga; assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch11_angles