proposition: Theorem Qcmp_shift_mult_l : ∀ x y z, 0 < z → (x / z ?= y) = (x ?= y * z).
proof: Proof. intros x y z Hz. erewrite Qmult_cmp_compat_r; [ idtac | eassumption ]. rewrite Qmult_div_swap. unfold Qdiv. rewrite <- Qmult_assoc. rewrite Qmult_inv_r; [ idtac | apply Qgt_0_not_0; assumption ]. rewrite Qmult_1_r; reflexivity. Qed.
imports: Utf8 QArith NPeano Sorted Psatz