lemma sh_nexts_le (h): sh_lt h → ∀s,n. s ≤ ⇡*[h,n]s.
#h #Hh #s #n @(nat_ind_succ … n) -n [ // ] #n #IH <sh_nexts_succ
lemma sh_nexts_le (h): sh_lt h → ∀s,n. s ≤ ⇡*[h,n]s.
#h #Hh #s #n @(nat_ind_succ … n) -n [ // ] #n #IH <sh_nexts_succ
[3: /3 width=1 by sh_next_lt, nlt_minus_bi_sn/ ]
<nminus_minus_dx_refl_sn [2,4: /2 width=1 by nlt_des_le/ ] -Hs21
[ * #n #H destruct
[3: /3 width=1 by sh_next_lt, nlt_minus_bi_sn/ ]
<nminus_minus_dx_refl_sn [2,4: /2 width=1 by nlt_des_le/ ] -Hs21
[ * #n #H destruct
| #H1 @or_intror * #n #H2 @H1 -H1 destruct
generalize in match Hs12; -Hs12
>(sh_nexts_zero h s1) in ⊢ (?%?→?); #H
lapply (sh_lt_nexts_inv_lt … Hh … H) -H #H
>(nlt_des_gen … H) -H
| #H1 @or_intror * #n #H2 @H1 -H1 destruct
generalize in match Hs12; -Hs12
>(sh_nexts_zero h s1) in ⊢ (?%?→?); #H
lapply (sh_lt_nexts_inv_lt … Hh … H) -H #H
>(nlt_des_gen … H) -H