Require Arith.
Require Minus.
Require Compare_dec.
Require Peano_dec.

Lemma minus_is_zero : (n,m:nat)(le n m)->(minus n m)=O. 

Intros n m.
Pattern n m .
Apply nat_double_ind.
Clear  n m.
Intros.
Simpl.
Reflexivity.
Clear  n m.
Intros.
Elim (le_Sn_O n).
Auto.
Clear  n m.
Intros.
Simpl.
Generalize (le_S_n n m H0).
Intros.
Apply (H H1).
Qed.

Lemma lt_minus_imp_lt : (k,n,m:nat)
    (le k n)->(le k m)->(lt (minus n k) (minus m k))->(lt n m).

Intros k n m.
Generalize k .
Clear  k.
Induction k.
Intros.
Rewrite <- (minus_n_O n) in H1.
Rewrite <- (minus_n_O m) in H1.
Auto.
Intros k'.
Intros.
Apply H.
Apply le_trans_S.
Auto.
Apply le_trans_S.
Auto.
Generalize (lt_n_S (minus n (S k')) (minus m (S k')) H2).
Intros.
Clear  H2.
Clear  H.
Rewrite (minus_Sn_m n (S k') H0) in H3.
Rewrite (minus_Sn_m m (S k') H1) in H3.
Simpl in H3.
Auto.
Qed.


Theorem lt_imp_lt_minus : (k,n,m:nat)
    (le k n)->(le k m)->(lt n m)->(lt (minus n k) (minus m k)).

Intros k n m.
Generalize k.
Induction k0.
Intros.
Rewrite <- (minus_n_O n).
Rewrite <- (minus_n_O m).
Auto.

Intros k'.
Intros.
Generalize (lt_n_S n m H2).
Generalize (le_trans_S k' n H0).
Intros.
Generalize (le_trans_S k' m H1).
Intros.
Generalize (H H3 H5 H2).
Intros.
Clear H H2.
Clear H3 H5.
Clear H4.
Cut (S (minus n (S k')))=(minus n k').
Intros.
Cut (S (minus m (S k')))=(minus m k').
Intros.
Rewrite <- H in H6.
Rewrite <- H2 in H6.
Clear H H2.
Apply lt_S_n.
Auto.

Rewrite (minus_Sn_m m (S k') H1).
Simpl.
Reflexivity.

Rewrite (minus_Sn_m n (S k') H0).
Simpl.
Reflexivity.
Qed.


Lemma lt_imp_lt_minus_l : (k,n,m:nat)(lt n m)->(lt (minus n k) m).

Intros.
Cut (le k n)->(lt (0) k)->(lt (minus n k) n).
Intros.
Elim (le_lt_dec k n).
Intros.
Elim (le_lt_dec k (0)).
Intros.
Generalize (le_n_O_eq k y0).
Intros.
Rewrite <- H1.
Rewrite <- (minus_n_O n).
Auto.
Intros.
Generalize (H0 y y0).
Intros.
Apply lt_trans with m:=n.
Auto.
Auto.
Intros.
Clear H0.
Generalize (lt_le_weak n k y).
Intros.
Rewrite (minus_is_zero n k H0).
Elim (zerop n).
Intros.
Rewrite y0 in H.
Auto.
Intros.
Apply lt_trans with m:=n.
Auto.
Auto.
Exact (lt_minus n k).
Qed.

Theorem lt_minus_imp_lt_minus : (m,n,k:nat)(le n m)->(le k m)->
  (lt (minus m n) k)->(lt (minus m k) n).

Intros.
Generalize (lt_reg_r ? ? n H1).
Intros.
Apply simpl_lt_plus_l with p:=k.
Rewrite le_plus_minus_r .
Rewrite (plus_sym (minus m n) n) in H2.
Rewrite (le_plus_minus_r n m H) in H2.
Trivial.
Trivial.
Qed.

Theorem le_minus : (m,n:nat)(le (minus m n) m).

Intros.
Pattern m n.
Apply nat_double_ind.
Intros.
Simpl.
Apply le_n.
Intros.
Simpl.
Apply le_n.
Intros.
Simpl.
Apply le_trans with 1:=H.
Apply le_n_Sn.
Qed.