proposition: Lemma average_realizer : forall e, average↓e ⊩ ∀₂q₁,q₂∈ℚ×ℚ, ℚ (Qcdiv (Qcplus q₁ q₂) 2%nat).
proof: Proof. Ksolve. apply Qq_realizer. find. start. apply ℚdiv_realizer. find. Qed.
imports: QArith Psatz ClassicalRealizability.Kbase ClassicalRealizability.Rationals