proposition: Lemma bet_per2__suma : forall A B C D E F G H I, A <> B -> B <> C -> D <> E -> E <> F -> G <> H -> H <> I -> Per A B C -> Per D E F -> Bet G H I -> SumA A B C D E F G H I.
proof: Proof. intros A B C D E F G H I H1 H2 H3 H4 H5 H6 HB HE HBet. destruct (ex_suma A B C D E F) as [G' [H' [I' HSuma]]]; auto. apply conga3_suma__suma with A B C D E F G' H' I'; [|apply conga_refl..|]; auto. assert_diffs. apply conga_line; auto. apply (per2_suma__bet A B C D E F); assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch11_angles