proposition: Lemma Qcmult_nonneg_nonneg x y : 0 ≤ x → 0 ≤ y → 0 ≤ x * y.
proof: Proof. intros. trans (0 * y); [by rewrite Qcmult_0_l|]. by apply Qcmult_le_mono_nonneg_r. Qed.
imports: Coq(QArith Qcanon) stdpp(well_founded) stdpp(options)