proposition: Lemma discrete_sum X Y : discrete X -> discrete Y -> discrete (X + Y).
proof: Proof. intros [d1] % discrete_iff [d2] % discrete_iff. eapply discrete_iff. econstructor. unfold dec. decide equality. all: solve [apply d1|apply d2]. Qed.
imports: Undecidability.Synthetic.Definitions Lia Undecidability.Shared.Dec Setoid Morphisms