(seq_n^ 1) - (seq_const 1) is eventually-positive by Lm54;