How to simplify A + 0 > 0 into A > 0?

I'm just a beginner with Coq, and I've been trying to prove a few elementary theorems about natural numbers. I've done a few already, not very elegantly, but completed nether the less. However I'm totally stuck on completing this theorem:

Theorem add_increase: (forall a b: nat, a > 0 -> a + b > b).
Proof.
  intros A.
  intros B.
  intros H.
  case B.

Entering this in, I get this output:

2 subgoals
A, B : nat
H : A > 0
______________________________________(1/2)
A + 0 > 0
______________________________________(2/2)
forall n : nat, A + S n > S n

Obviously, the first goal is pretty trivial to simplify to hypothesis H. However, I just can't figure out how to make this straightforward simplification.

Solution

One way to simplify this is to use a rather boring lemma

Lemma add_zero_r : forall n, n + 0 = n.
Proof.
  intros n. induction n. reflexivity.
  simpl. rewrite IHn. reflexivity.
Qed.

and next use this to rewrite your goal:

Theorem add_increase: (forall a b: nat, a > 0 -> a + b > b).
Proof.
  intros A.
  intros B.
  intros H.
  case B.
  rewrite (add_zero_r A).
  assumption.

To finish the other proof case I've used a little lemma and a tactic that eases the task of proving stuff with inequalities over naturals.

First, I've imported Omega library.

Require Import Omega.

Prove another boring fact.

Lemma add_succ_r : forall n m, n + (S m) = S (n + m).
Proof.
  intros n m. induction n. reflexivity.
  simpl. rewrite IHn. reflexivity.
Qed.

and going back to add_increase prove we have the following goal:

A, B : nat
H : A > 0
============================
forall n : nat, A + S n > S n

That can be solved by:

 intros C.
 rewrite (add_succ_r A C).
 omega.

Again, I've used the previous proved lemma to rewrite the goal. The omega tactic is a very useful one since it is a complete decision procedure for the so called quantifier free Presburger arithmetic, and based on your context, it can solve the goal automagically.

Here's the complete solution to your proof:

 Require Import Omega.

 Lemma add_zero_r : forall n, n + 0 = n.
 Proof.
   intros n. induction n. reflexivity.
   simpl. rewrite IHn. reflexivity.
 Qed.

 Lemma add_succ_r : forall n m, n + (S m) = S (n + m).
 Proof.
  intros n m. induction n. reflexivity.
  simpl. rewrite IHn. reflexivity.
 Qed.

Theorem add_increase: (forall a b: nat, a > 0 -> a + b > b).
Proof.
  intros A.
  intros B.
  intros H.
  case B.
  rewrite (add_zero_r A).
  assumption.
  intros C.
  rewrite (add_succ_r A C).
  omega.
 Qed.