law range_succ_sym

bend-mathlib@0.8.1.0 · list.bend:3091

import Base

3091# Range(n + 1) is range(n) followed by n, reversed to rewrite toward the simple side.
3092law range_succ_sym:
3093  for n: Nat
3094  {List.append(&2, Nat, List.range(n), [n]) == List.range(1n+n) : List<&2, Nat>}