proposition: Lemma trisuma_perm_321 : forall A B C D E F, TriSumA A B C D E F -> TriSumA C B A D E F.
proof: Proof. intros A B C D E F HT. destruct HT as [A1 [B1 [C1 [HT1 HT2]]]]. apply suma_sym in HT2. assert_diffs. assert(Hex:= ex_suma C A B A B C). destruct Hex as [C2 [A2 [B2 Hex]]]; auto. exists C2. exists A2. exists B2. split. SumA. apply suma_middle_comm. apply (suma_assoc C A B A B C B C A D E F C2 A2 B2 A1 B1 C1); try (apply sams123231); auto. Qed.
imports: GeoCoq.Tarski_dev.Ch11_angles