proposition: Lemma lt_add_l p q : p < p + q.
proof: Proof. destruct p as [p ?], q as [q ?]. apply to_Qc_inj_lt; simpl. rewrite <- (Qcplus_0_r p) at 1. by rewrite <-Qcplus_lt_mono_l. Qed.
imports: Coq(QArith Qcanon) stdpp(well_founded) stdpp(options)