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