proposition: Lemma ex_defect : forall A B C, A <> B -> B <> C -> A <> C -> exists D E F, Defect A B C D E F.
proof: Proof. intros A B C HAB HBC HAC. destruct (ex_trisuma A B C) as [G [H [I HTri]]]; auto. suma.assert_diffs. destruct (ex_suppa G H I) as [D [E [F HSuppa]]]; auto. exists D, E, F, G, H, I. split; assumption. Qed.
imports: GeoCoq.Tarski_dev.Annexes.saccheri