+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-include "ground/relocation/gr_basic.ma".
-include "ground/relocation/gr_nat_uni.ma".
-
-(* NON-NEGATIVE APPLICATION FOR GENERIC RELOCATION MAPS *********************)
-
-(* Constructions with gr_basic **********************************************)
-
-lemma gr_nat_basic_lt (m) (n) (l):
- l < m ā @āāŖl, šāØm,nā©ā« ā l.
-#m @(nat_ind_succ ā¦ m) -m
-[ #n #i #H elim (nlt_inv_zero_dx ā¦ H)
-| #m #IH #n #l @(nat_ind_succ ā¦ l) -l
- [ #_ /2 width=2 by refl, gr_pat_refl/
- | #l #_ #H
- lapply (nlt_inv_succ_bi ā¦ H) -H #Hlm
- /3 width=7 by refl, gr_pat_push/
- ]
-]
-qed.
-
-lemma gr_nat_basic_ge (m) (n) (l):
- m ā¤ l ā @āāŖl, šāØm,nā©ā« ā l+n.
-#m @(nat_ind_succ ā¦ m) -m //
-#m #IH #n #l #H
-elim (nle_inv_succ_sn ā¦ H) -H #Hml #H >H -H
-/3 width=7 by gr_nat_push/
-qed.
-
-(* Inversions with gr_basic *************************************************)
-
-lemma gr_nat_basic_inv_lt (m) (n) (l) (k):
- l < m ā @āāŖl, šāØm,nā©ā« ā k ā l = k.
-/3 width=4 by gr_nat_basic_lt, gr_nat_mono/ qed-.
-
-lemma gr_nat_basic_inv_ge (m) (n) (l) (k):
- m ā¤ l ā @āāŖl, šāØm,nā©ā« ā k ā l+n = k.
-/3 width=4 by gr_nat_basic_ge, gr_nat_mono/ qed-.