(* Exercise coq_nat_11 *)

(* Do you know that having stamps of nominals 3 and 5 you can
   pay any value greater or equal than 8? 
   Below is a Coq specification of this statemant - can you
   prove it? *)
Require Import Arith.

(* Hint: for arithmetical reasoning you may try to use the 
         'omega' tactic. If you do that you will only get
	 Correct for this exercise (and not Solved), as this 
	 is one of the powerful automated Coq tactics, that 
	 are in principle not allowed to be used for solving
	 those exercises. In this case, however, it is ok
	 to use omega.
	 
   Remark: if afterwards you decide to try to prove it without
           the use of omega, it should give you a good idea
	   of how helpful such automated tactics can be!
*)   
Require Import Omega.

Lemma stamps : forall i, exists v3, exists v5, i + 8 = 3*v3 + 5*v5.

Proof.
induction i.
exists 1.
exists 1.
auto.
destruct IHi.
destruct H.
destruct x0.
destruct x.
simpl in H.
(* the context is inconsistent and we can prove that using "omega"
   omega can solve simple arithmetic goals that have no quantifiers
   so we proceed as follows *)
assert (~(i+8 = 0)).
omega.
contradiction.
destruct x.
simpl in H.

(* we are in a similar situation as before, but we now do it a bit
   simpler by chaining tactics the "by" tells assert which tactics
   should be used to prove the asserted formula*)
assert (~ (i + 8 = 3)) by omega.
contradiction.
destruct x.
simpl in H.
(* even shorter *)
assert (~ (i + 8 = 6)) by omega; contradiction.
exists x.
exists 2.
omega.
exists (x+2).
exists x0.
omega.
Qed.