proposition: Lemma QnonNeg_mid (x y: QnonNeg): ` x < ` y -> let mid := ((1#2) * (x + y))%Qnn in ` x < ` mid /\ ` mid < ` y.
proof: Proof. intros. subst mid. simpl. apply Qmid. assumption. Qed.
imports: Coq.QArith.Qabs CoRN.model.ordfields.Qordfield CoRN.model.structures.Qpossec Coq.QArith.Qminmax Coq.setoid_ring.Ring Coq.Program.Program