plus.v

Inductive nat : Type :=
 | O : nat
 | S : nat -> nat.

Inductive bool : Type :=
 | true : bool
 | false: bool.


Fixpoint lessthan (n : nat) (m : nat) : bool :=
 match n with
   | O => 
        match m with
          | O => false
          | S m' => true
        end
   | S n' =>
        match m with
          | O => false
          | S m' => (lessthan n' m')
        end
  end.

Fixpoint plus (n m : nat) : nat :=
  match m with
    | O => n
    | S m' => S (plus n m')
  end.


Theorem lessthan_th1 : 
  forall (n : nat) , (lessthan n (S n)) = true.
Proof.
  intros.
  induction n.
  simpl.
  reflexivity.
  simpl.
  rewrite -> IHn.
  reflexivity.
Qed.

Theorem plus_th1 :
  forall (n : nat) , (plus O n) = n.
Proof.
  intros.
  induction n.
  simpl.
  reflexivity.
  simpl.
  rewrite -> IHn.
  reflexivity.
Qed.

Theorem plus_th2 : 
  forall (n m : nat) , (S (plus n m)) = (plus (S n) m).
Proof.
  intros.
  induction m.
  simpl.
  reflexivity.
  simpl.
  rewrite <- IHm.
  reflexivity.
Qed.

Theorem plus_th3 : 
  forall (n m : nat) , (plus n m) = (plus m n).
Proof.
  intros.
  induction m.
  rewrite -> plus_th1.
  simpl.
  reflexivity.
  simpl.
  rewrite -> IHm.
  rewrite <- plus_th2.
  reflexivity.
Qed.