proposition: Lemma Qeq_eqR : forall x y : Q, x==y -> Q2R x = Q2R y.
proof: Proof. unfold Qeq, Q2R; intros (x1, x2) (y1, y2); unfold Qnum, Qden; intros. set (X1 := IZR x1) in *; assert (X2nz := IZR_nz x2); set (X2 := IZR (Zpos x2)) in *. set (Y1 := IZR y1) in *; assert (Y2nz := IZR_nz y2); set (Y2 := IZR (Zpos y2)) in *. assert ((X1 * Y2)%R = (Y1 * X2)%R). - unfold X1, X2, Y1, Y2; do 2 rewrite <- mult_IZR. f_equal; auto. - clear H. field_simplify_eq; auto. rewrite H0; ring. Qed.
imports: Rdefinitions Raxioms RIneq QArith_base