proposition: Lemma sums_sym : forall A B C D E F, SumS A B C D E F -> SumS C D A B E F.
proof: Proof. intros A B C D E F HSumS. destruct HSumS as [P [Q [R [HBet [HCong1 [HCong2 HCong3]]]]]]. exists R, Q, P. repeat split; Between; Cong. Qed.
imports: GeoCoq.Tarski_dev.Ch06_out_lines