law range_succ

bend-mathlib@0.8.1.0 · list.bend:1987

import Base

1987# Range(n + 1) is range(n) followed by n.
1988law range_succ:
1989  for n: Nat
1990  {List.range(1n+n) == List.append(&2, Nat, List.range(n), [n]) : List<&2, Nat>}