##[nrewrite > (le_to_leb_true ?? Hnk);nnormalize;//;
##|nrewrite > (lt_to_leb_false (S (n + 1)) k ?); nnormalize;
##[nrewrite > (not_eq_to_eqb_false (n+1) k ?);
- nnormalize;/2/; napply (not_to_not … Hnk);//;
+ nnormalize;/2/
##|napply le_S; napplyS (not_le_to_lt (S n) k Hnk);
##]
##]