Fixpoint leb (n m:nat) : bool :=
  match n with O => true
           | S p => match m with O => false
                             | S q => leb p q
                     end
  end.

Eval compute in (leb 4 5).
Eval compute in (leb 5 4).
Eval compute in fun n => (leb n (S n)).

Lemma leb_simpl : forall n m, 
  leb n m = match n with O => true
           | S p => match m with O => false
                             | S q => leb p q
                    end
  end.
intros.
destruct n; trivial.
Save.
  
Print plus.
Goal forall n m, (S n) + m = S (n+m).
simpl.
reflexivity.
Save.

(*
Goal forall n m, n + (S m) = S (n+m).
simpl.
(* Induction needed *)
*)

(*
Fixpoint test (n m:nat) (b:bool) {struct m} 
  := match (n,m) with 
   (O,_)   => true
 | (_,0)   => false
 | (S p,S q) => if b then test p m b else test n q b
 end.
*)

Fixpoint ack (n m:nat) {struct n} := match n with 
   0   => S m
 | S p => let fix ackn (m:nat) {struct m} := 
              match m with 0  => ack p 1
                        | S q => ack p (ackn q)
              end
          in ackn m
end.

Lemma ack_Sn_0 : forall n, ack (S n) 0 = ack n 1.
reflexivity.
Save.

Lemma ack_Sn_Sm : forall n m, 
      ack (S n) (S m) = ack n (ack (S n) m).
reflexivity.
Save.



(* Empty types *)
Inductive E : Type := Ei : E -> E.
Fixpoint Eany (A:Type) (x : E) : A := 
   match x with (Ei y) => Eany A y end.