proposition: Lemma suma_distincts : forall A B C D E F G H I, SumA A B C D E F G H I -> A<>B /\ B<>C /\ D<>E /\ E<>F /\ G<>H /\ H<>I.
proof: Proof. intros A B C D E F G H I Hsuma. destruct Hsuma as [J HJ]. spliter. assert_diffs. repeat split; auto. Qed.
imports: GeoCoq.Tarski_dev.Ch11_angles