proposition: Theorem dichotomy : forall x y e, D↓e ⊩ (x ≤ y ∨ y ≤ x).
proof: Proof. Ksolve. unfold Rle. Ksolve. unfold Rle. Kmove. destruct (Qclt_le_dec q' q0). Ksolve. apply (sub_stack Hπ0). now apply (↓y). Ksolve. apply (sub_stack Hπ1). apply (↓x). revert Hc Hc0 q1. Qcunfold. lra. Qed.
imports: QArith Psatz ClassicalRealizability.Kbase ClassicalRealizability.Rationals