proposition: Lemma Qmult_pos_r : forall x y : Q, 0 <= x -> 0 < x * y -> 0 < y.
proof: Proof. intros x y H1 H2. destruct (Q_dec y 0) as [[? | ?] | H]; trivial. + exfalso. apply (Qlt_irrefl 0), Qlt_le_trans with (y := x * y); trivial. now apply Qmult_nonneg_nonpos; [| apply Qlt_le_weak]. + rewrite H, Qmult_0_r in H2. exfalso; now apply (Qlt_irrefl 0). Qed.
imports: Coq.QArith.QArith Coq.ZArith.ZArith Coq.NArith.NArith Coq.QArith.Qpower Coq.QArith.Qround Coq.QArith.Qround Coq.QArith.Qabs CoRN.stdlib_omissions.List