include "ground/arith/pnat_lt.ma".
include "ground/relocation/gr_pat.ma".
-(* POSITIVE APPLICATION FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* POSITIVE APPLICATION FOR GENERIC RELOCATION MAPS *************************)
-(* Forward lemmas with plt and ple *****************************************************)
+(* Destructions with plt and ple ********************************************)
(*** at_increasing *)
lemma gr_pat_increasing (i2) (i1) (f):
qed-.
(*** at_fwd_id_ex *)
-lemma gr_pat_des_id (f) (i): @â\9dªi,fâ\9d« â\89\98 i â\86\92 ⫯⫱f = f.
+lemma gr_pat_des_id (f) (i): @â\9dªi,fâ\9d« â\89\98 i â\86\92 ⫯⫰f = f.
#f elim (gr_map_split_tl f) //
#H #i #Hf elim (gr_pat_inv_next … Hf … H) -Hf -H
#j2 #Hg #H destruct lapply (gr_pat_increasing … Hg) -Hg
#H elim (plt_ge_false … H) -H //
qed-.
-(* Properties with ple *********************************************************)
+(* Constructions with ple ***************************************************)
(*** at_le_ex *)
lemma gr_pat_le_ex (j2) (i2) (f):