proposition: Theorem Qmult_cmp_compat_r : ∀ x y z, 0 < z → (x ?= y) = (x * z ?= y * z).
proof: Proof. intros (a₁, a₂) (b₁, b₂) (c₁, c₂) H. unfold Qcompare; simpl. do 2 rewrite Pos2Z.inj_mul. rewrite Z.mul_shuffle1, (Z.mul_shuffle1 b₁). rewrite <- Zmult_cmp_compat_r; [ reflexivity | idtac ]. apply Z.mul_pos_pos; [ idtac | reflexivity ]. unfold Qlt in H; simpl in H. rewrite Zmult_1_r in H; assumption. Qed.
imports: Utf8 QArith NPeano Sorted Psatz