law length_range_sym

bend-mathlib@0.8.1.0 · list.bend:2407

import Base

2407# Range(n) has length n, reversed to rewrite toward the simple side.
2408law length_range_sym:
2409  for n: Nat
2410  {n == List.length(&2, Nat, List.range(n)) : Nat}