(* 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 
         'lia' tactic. 
   This is one of the powerful automated Coq tactics, that 
	 solves problems in linear arithmetic. 
   In the first exercises we did, I advised you to not use
   too much automation, because it is good to understand the
   underlying principles. In general, and also for the assignment,
   it is ok to use lia.
	 
   Remark: if afterwards you decide to try to prove it without
           the use of lia, it should give you a good idea
	   of how helpful such automated tactics can be!
*)   

Require Import Lia.

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. (* distinguishing cases x0 = 0 or x0 = S x1 *)
   * destruct x. (* distinguishing cases x = 0 or x = S x2 *)
     + simpl in H.
       (* it can be shown that the context is inconsistent using 
          some simple arithmetic, and we can prove that using "lia"
          lia can solve simple arithmetic goals that have no quantifiers
          so we proceed as follows 
          one could also do
              assert (~(i+8 = 0)).
              lia.
              contradiction.
        *)
        lia.
     + destruct x. (* distinguishing cases x = 0 or x = S x2 *)
       -- simpl in H.
       (* we are in a similar situation as before, the context is 
          inconsistent using some simple arithmetic *)
          lia.
       -- destruct x.
          ** simpl in H.
             lia.
          (* Now the real choices have to be made! *)
          ** exists x.
             exists 2.
             lia.
   * exists (x+2).
     exists x0.
     lia.
Qed.