proposition: Lemma discrete_iff X : discrete X <-> inhabited (eq_dec X).
proof: Proof. split. - intros [D] % decidable_iff. econstructor. intros x y; destruct (D (x,y)); firstorder. - intros [d]. eapply decidable_iff. econstructor. intros (x,y). eapply d. Qed.
imports: Undecidability.Synthetic.Definitions Lia Undecidability.Shared.Dec Setoid Morphisms