proposition: Theorem le_sub_le_add_l : ∀ n m p, n - m ≤ p → n ≤ m + p.
proof: Proof. intros n m p H. destruct m as [m| ]; [ idtac | constructor ]. destruct p as [p| ]; [ idtac | rewrite add_comm; constructor ]. destruct n as [n| ]; [ simpl in H; simpl | inversion H ]. apply le_qfin. apply qfin_le_mono in H. apply Qle_sub_le_add_l; assumption. Qed.
imports: Utf8 QArith Misc