proposition: Lemma suma_right_comm : forall A B C D E F G H I, SumA A B C D E F G H I -> SumA A B C D E F I H G.
proof: Proof. intros A B C D E F G H I Hsuma. assert(Hd := suma_distincts A B C D E F G H I Hsuma). spliter. apply (conga3_suma__suma A B C D E F G H I); CongA. Qed.
imports: GeoCoq.Tarski_dev.Ch11_angles