proposition: Lemma bet_suppa__suma : forall A B C D E F G H I, G <> H -> H <> I -> SuppA A B C 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; intros. assert_diffs. destruct (ex_suma A B C D E F) as [G' [H' [I']]]; auto. apply (conga3_suma__suma A B C D E F G' H' I'); try apply conga_refl; auto. assert_diffs. apply conga_line; auto. apply (suma_suppa__bet A B C D E F); assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch11_angles