proposition: Lemma dec_compl X p : decidable p -> decidable (fun x : X => ~ p x).
proof: Proof. intros [f H]. exists (fun x => negb (f x)). intros x. eapply reflects_not, H. Qed.
imports: Undecidability.Synthetic.Definitions Lia Undecidability.Shared.Dec Setoid Morphisms