proposition: Lemma Qcmult_pos_pos x y : 0 < x → 0 < y → 0 < x * y.
proof: Proof. intros. apply Qcle_lt_trans with (0 * y); [by rewrite Qcmult_0_l|]. by apply Qcmult_lt_mono_pos_r. Qed.
imports: Coq(QArith Qcanon) stdpp(well_founded) stdpp(options)