Cut-off Subtraction in Coq

Question

I am new to the world of computer assistant proof programs in general, and Coq in particular. As a result, I have sought to prove some elementary results about integers as a way to … At the moment, I am dealing with cut-off subtraction. This I have defined in Coq to be:

Definition monus (m n:N):N := R (fun x=> N) m (fun x y=> pd y) n.

where pd represents the predecessor function

Definition pd (n: N): N := R (fun _=> N) zero (fun x y=> x) n

What I want to accomplish is to first prove that for all $m,n \in\mathbb{N}$ \begin{equation} S(m)-S(n)=m-n \tag{*}\end{equation} and then prove \begin{equation} (m+n)-n=m \tag{**} \end{equation}

These are displayed in Coq as:

1. Lemma monus_eq3 : (forall m n:N, I N (monus (succ m) (succ n)) (monus m n)).
2. Lemma monus_eq4 : (forall m n:N, I N (monus (add m n) n) m).

This is what I have managed to write at this stage:

(* Sigma types *)


Inductive Sigma (A:Set)(B:A -> Set) :Set :=
  Spair: forall a:A, forall b : B a,Sigma A B.

Definition E (A:Set)(B:A -> Set)
  (C: Sigma A B -> Set)
  (c: Sigma A B)
  (d: (forall x:A, forall y:B x, 
      C (Spair A B x y))): C c :=

match c as c0 return (C c0) with
| Spair a b => d a b
end. 


(* Binary sum type *)

Inductive sum' (A B:Set):Set := 
inl': A -> sum' A B | inr': B -> sum' A B.

Print sum'_rect.

Definition D (A B : Set)(C: sum' A B -> Set)
(c: sum' A B)
(d: (forall x:A, C (inl' A B x)))
(e: (forall y:B, C (inr' A B y))): C c :=

match c as c0 return C c0 with
| inl' x => d x
| inr' y => e y
end.

(* Three useful finite sets *)

Inductive N_0: Set :=.

Definition R_0
  (C:N_0 -> Set)
  (c: N_0): C c :=
match c as c0 return (C c0) with
end.

Inductive N_1: Set := zero_1:N_1.

Definition R_1 
  (C:N_1 -> Set)
  (c: N_1)
  (d_zero: C zero_1): C c :=
match c as c0 return (C c0) with
  | zero_1 => d_zero
end.

Inductive N_2: Set := zero_2:N_2 | one_2:N_2.

Definition R_2 
  (C:N_2 -> Set)
  (c: N_2)
  (d_zero: C zero_2)
  (d_one: C one_2): C c :=
match c as c0 return (C c0) with
  | zero_2 => d_zero
  | one_2  => d_one
end.


(* Natural numbers *)

Inductive N:Set :=
zero: N | succ : N -> N.

Print N. 

Print N_rect.

Definition R 
  (C:N -> Set)
  (d: C zero)
  (e: (forall x:N, C x -> C (succ x))):
  (forall n:N, C n) :=
fix F (n: N): C n :=
  match n as n0 return (C n0) with
  | zero => d
  | succ n0 => e n0 (F n0)
  end.

(* Boolean to truth-value converter *)

Definition Tr (c:N_2) : Set :=
match c as c0 with
  | zero_2 => N_0
  | one_2 => N_1
end.

(* Identity type *)

Inductive I (A: Set)(x: A) : A -> Set :=
r :  I A x x.

Print I_rect.

Theorem J 
  (A:Set)
  (C: (forall x y:A, 
              forall z: I A x y, Set))
  (d: (forall x:A, C x x (r A x)))
  (a:A)(b:A)(c:I A a b): C a b c.
induction c.
apply d.
Defined.

(* functions are extensional wrt
  identity types *)

Theorem I_I_extensionality (A B: Set)(f: A -> B):
(forall x y:A, I A x y -> I B (f x) (f y)).
Proof.
intros x y P.
induction P.
apply r.
Defined.


(* addition *)

Definition add (m n:N) : N 
 := R (fun z=> N) m (fun x y => succ y) n.

(* multiplication *)

Definition mul (m n:N) : N 
 := R (fun z=> N) zero (fun x y => add y m) n.


(* Axioms of Peano verified *)

Theorem P1a: (forall x: N, I N (add x zero) x).
intro x.
(* force use of definitional equality
  by applying reflexivity *)
apply r.
Defined.


Theorem P1b: (forall x y: N, 
I N (add x (succ y)) (succ (add x y))).
intros.
apply r.
Defined.


Theorem P2a: (forall x: N, I N (mul x zero) zero).
intros.
apply r.
Defined.


Theorem P2b: (forall x y: N, 
I N (mul x (succ y)) (add (mul x y) x)).
intros.
apply r.
Defined.

Definition pd (n: N): N :=
R (fun _=> N) zero (fun x y=> x) n.

(* alternatively
Definition pd (x: N): N :=
match x as x0 with
  | zero => zero
  | succ n0 => n0
end.
*)

Theorem P3: (forall x y:N, 
I N (succ x) (succ y) -> I N x y).
intros x y p.
apply (I_I_extensionality N N pd (succ x) (succ y)).
apply p.
Defined.

Definition not (A:Set): Set:= (A -> N_0).

Definition isnonzero (n: N): N_2:=
R (fun _ => N_2) zero_2 (fun x y => one_2) n.


Theorem P4 : (forall x:N, 
not (I N (succ x) zero)).
intro x.
intro p.

apply (J N (fun x y z => 
    Tr (isnonzero x) -> Tr (isnonzero y))
    (fun x => (fun t => t)) (succ x) zero)
.
apply p.
simpl.
apply zero_1.
Defined.

Theorem P5 (P:N -> Set):
P zero -> (forall x:N, P x -> P (succ x))
   -> (forall x:N, P x).
intros base step n.
apply R.
apply base.
apply step.
Defined.

(* I(A,-,-) is an equivalence relation *)

Lemma Ireflexive (A:Set): (forall x:A, I A x x).
intro x.
apply r.
Defined.

Lemma Isymmetric (A:Set): (forall x y:A, I A x y -> I A y x).
intros x y P.
induction P.
apply r.
Defined.

Lemma Itransitive (A:Set): 
(forall x y z:A, I A x y -> I A y z -> I A x z).
intros x y z P Q.
induction P.
assumption.
Defined.


Lemma succ_cong : (forall m n:N, I N m n -> I N (succ m) (succ n)).
intros m n H.
induction H.
apply r.
Defined.

Lemma zeroadd: (forall n:N, I N (add zero n) n).
intro n.
induction n.
simpl.
apply r.
apply succ_cong.
auto.

Defined.

Lemma succadd: (forall m n:N, I N (add (succ m) n) (succ (add m n))).
intros.
induction n.
simpl.
apply r.
simpl.
apply succ_cong.
auto.

Defined.

Lemma commutative_add: (forall m n:N, I N (add m n) (add n m)).
intros n m; elim n.
apply zeroadd.
intros y H; elim (succadd m y).
simpl.
rewrite succadd.
apply succ_cong.
assumption.


Defined.

Lemma associative_add: (forall m n k:N, 
I N (add (add m n) k) (add m (add n k))).
intros m n k.
induction k.
simpl.
apply Ireflexive.
simpl.
apply succ_cong.
assumption.
Defined.

(* modified subtraction *)

Definition monus (m n:N):N := R (fun x=> N) m (fun x y=> pd y) n.

Lemma monus_eq1 :
(forall n:N, I N (monus n zero) n).
intro m.
induction m.
apply Ireflexive.
simpl.
apply Ireflexive.

Defined.

Lemma monus_eq2 :
(forall m:N, I N (monus zero m) zero).
intro m.
induction m.
apply Ireflexive.
simpl.
(* induction IHm. fails - try apply to the symmetric equality *)
assert (I N zero (monus zero m)) as IHm_symm.
apply Isymmetric.
assumption.
induction IHm_symm.
apply Ireflexive.

Defined.

Lemma monus_eq3 :
(forall m n:N, I N (monus (succ m) (succ n)) (monus m n)).
intros.
induction m.
simpl.


(* Here is where I need your help *)



Lemma monus_eq4 :
(forall m n:N, I N (monus (add m n) n) m).

(* Here as well *)

My problem starts when I induct on Lemma monus_eq3; I literally get stuck immediately(!). The goal is not in a form in which I can use any of my previous results. That is why I am now, after some considerable effort, turn to you in the hope that you may be so kind as to relieve me from this frustrating "stuck state". All help is sincerely appreciated!