proposition: Lemma Rlt_Qlt : forall x y : Q, (Q2R x < Q2R y)%R -> x<y.
proof: Proof. unfold Qlt, Q2R; intros (x1, x2) (y1, y2); unfold Qnum, Qden; intros. apply lt_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 *. replace (X1 * Y2)%R with (X1 * / X2 * (X2 * Y2))%R; try (field; auto). replace (Y1 * X2)%R with (Y1 * / Y2 * (X2 * Y2))%R; try (field; auto). apply Rmult_lt_compat_r; auto. apply Rmult_lt_0_compat. - now apply IZR_lt. - now apply IZR_lt. Qed.
imports: Rdefinitions Raxioms RIneq QArith_base