proposition: Lemma suma__suppa : forall A B C D E F, SumA A B C B C A D E F -> SuppA D E F C A B.
proof: Proof. intros A B C D E F HSuma. suma.assert_diffs. destruct (point_construction_different A B) as [A' []]. apply bet_suma__suppa with A B A'; trivial. apply bet_suma__suma; auto. Qed.
imports: GeoCoq.Tarski_dev.Annexes.circles GeoCoq.Tarski_dev.Annexes.half_angles GeoCoq.Tarski_dev.Ch12_parallel_inter_dec