proposition: Fact reduces_complement : P ⪯ Q -> complement P ⪯ complement Q.
proof: Proof. intros [f Hf]. exists f. intros x. specialize (Hf x). split. all: intros H Hc; apply H, Hf, Hc. Qed.
imports: Undecidability.Synthetic.Definitions