proposition: Theorem Qlt_shift_mult_r : ∀ x y z, 0 < z → x < y / z → x * z < y.
proof: Proof. intros x y z Hc H. rewrite Qlt_alt in H |- *. rewrite <- H; symmetry; apply Qcmp_shift_mult_r; assumption. Qed.
imports: Utf8 QArith NPeano Sorted Psatz