proposition: Lemma bet_suma__suma : forall A B C D E F G H I, G <> H -> H <> I -> Bet G H I -> SumA A B C B C A D E F -> SumA D E F C A B G H I.
proof: Proof. intros A B C D E F G H I HGH HHI HBet HSuma. suma.assert_diffs. destruct (bet__trisuma A B C G H I) as [D' [E' [F' []]]]; auto. apply (conga3_suma__suma D' E' F' C A B G H I); try apply conga_refl; auto. apply (suma2__conga A B C B C A); assumption. Qed.
imports: GeoCoq.Tarski_dev.Annexes.circles GeoCoq.Tarski_dev.Annexes.half_angles GeoCoq.Tarski_dev.Ch12_parallel_inter_dec