proposition: Lemma Rle_refl_realizer : forall x e, Rle_refl↓e ⊩ x ≤ x.
proof: Proof. unfold Rle. intros. start. apply (sub_term Ht (B:=x[q'])). now apply (↓x q). ok. Qed.
imports: QArith Psatz ClassicalRealizability.Kbase ClassicalRealizability.Rationals