proposition: Lemma defect_distincts : forall A B C D E F, Defect A B C D E F -> A <> B /\ B <> C /\ A <> C /\ D <> E /\ E <> F.
proof: Proof. intros A B C D E F HDef. destruct HDef as [G [H [I [HTri HSuppa]]]]. suma.assert_diffs. repeat split; auto. Qed.
imports: GeoCoq.Tarski_dev.Annexes.saccheri