proposition: Lemma out546__suma : forall A B C D E F, A <> B -> B <> C -> Out E D F -> SumA A B C D E F A B C.
proof: Proof. intros A B C D E F HAB HBC Hout. assert_diffs. destruct (ex_suma A B C D E F) as [G [H [I Hsuma]]]; auto. apply (conga3_suma__suma A B C D E F G H I); try (apply conga_refl); auto. apply conga_sym, out546_suma__conga with D E F; auto. Qed.
imports: GeoCoq.Tarski_dev.Ch11_angles