proposition: Lemma plus_homo (x y: QnonNeg): (x + y)%Qnn == x + y.
proof: Proof. Proof with auto. unfold eq, le. simpl. split; intros. inversion H. subst. clear H. apply Qle_trans with (`q)... apply Qle_trans with (`q0 + `q')%Q... apply Qplus_le_compat... apply (is_binop_bound Qplus) with x y... apply Qle_trans with (`q)... Qed.
imports: Coq.QArith.Qabs CoRN.model.ordfields.Qordfield CoRN.model.structures.Qpossec Coq.QArith.Qminmax Coq.setoid_ring.Ring Coq.Program.Program