#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-.
#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-.