proposition: Lemma defect_perm_231 : forall A B C D E F, Defect A B C D E F -> Defect B C A D E F.
proof: Proof. intros A B C D E F HDef. destruct HDef as [G [H [I [HTri HSuppa]]]]. exists G, H, I. split; trivial. apply trisuma_perm_231, HTri. Qed.
imports: GeoCoq.Tarski_dev.Annexes.saccheri