proposition: Lemma Rle_trans_realizer : forall x y z e, Rle_trans↓e ⊩ x ≤ y → y ≤ z → x ≤ z.
proof: Proof. unfold Rle. Ksolve. apply average_realizer. find. Ksolve. rewrite Qclt_shift_div_l. replace (q' * 2%Z) with (q' + q')%Qc. now apply Qcplus_lt_le_compat. Qcunfold. simpl. ring. now compute. Ksolve. rewrite Qclt_shift_div_r. replace (q * 2%Z) with (q + q)%Qc. now apply Qcplus_le_lt_compat. Qcunfold. simpl. ring. now compute. Qed.
imports: QArith Psatz ClassicalRealizability.Kbase ClassicalRealizability.Rationals