proposition: Lemma Qpos_lt_1_mult_l (x : Qpos) (y : Q) : (y < 1 → y * proj1_sig x < proj1_sig x)%Q.
proof: Proof. Proof with auto with qarith. intros E. destruct x; simpl. rewrite <-(Qmult_1_l x), Qmult_assoc. apply Qmult_lt_compat_r. exact q. rewrite Qmult_1_r. exact E. Qed.
imports: CoRN.metric2.Metric CoRN.model.totalorder.QposMinMax Coq.Setoids.Setoid CoRN.stdlib_omissions.Q CoRN.model.totalorder.QMinMax CoRN.metric2.Complete CoRN.metric2.Prelength MathClasses.interfaces.abstract_algebra