proposition: Lemma Qcplus_pos_nonneg (x y : Qc) : 0 < x → 0 ≤ y → 0 < x + y.
proof: Proof. intros. apply Qclt_le_trans with (x + 0); [by rewrite Qcplus_0_r|]. by apply Qcplus_le_mono_l. Qed.
imports: Coq(QArith Qcanon) stdpp(well_founded) stdpp(options)