proposition: Lemma eqR_Qeq : forall x y : Q, Q2R x = Q2R y -> x==y.
proof: Proof. unfold Qeq, Q2R; intros (x1, x2) (y1, y2); unfold Qnum, Qden; intros. apply eq_IZR. do 2 rewrite mult_IZR. 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 ((X2 * X1 * / X2)%R = (X2 * (Y1 * / Y2))%R). - rewrite <- H; field; auto. - rewrite Rinv_r_simpl_m in H0; auto; rewrite H0; field; auto. Qed.
imports: Rdefinitions Raxioms RIneq QArith_base