proposition: Lemma Req_trans_realizer : forall x y z e, Req_trans↓e ⊩ x ≡ y → y ≡ z → x ≡ z.
proof: Proof. unfold Req. repeat Ksolve; eapply Rle_trans_realizer; find. Qed.
imports: QArith Psatz ClassicalRealizability.Kbase ClassicalRealizability.Rationals