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