proposition: Lemma divℚ_realizer : forall p q tp tq e, tp↓e ⊩ ℚ p -> tq↓e ⊩ ℚ q -> (divℚ @ tp @ tq)↓e ⊩ ℚ (p/q).
proof: Proof. unfold divℚ, caron2. Kmove. exists (ℚ q → ℚ (p/q)). do 3 Ksolve. apply ℚdiv_realizer. find. Qed.
imports: QArith ClassicalRealizability.Qcabs ClassicalRealizability.Qcminmax ClassicalRealizability.Kbase