##[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 ?);
##[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 ?);