proposition: Lemma Q2R_plus : forall x y : Q, Q2R (x+y) = (Q2R x + Q2R y)%R.
proof: Proof. unfold Qplus, Qeq, Q2R; intros (x1, x2) (y1, y2); unfold Qden, Qnum. simpl_mult. rewrite plus_IZR. do 3 rewrite mult_IZR. field; auto. Qed.
imports: Rdefinitions Raxioms RIneq QArith_base