law length_range

bend-mathlib@0.8.1.0 · list.bend:420

import Base

420# Range(n) has length n.
421law length_range:
422  for n: Nat
423  {List.length(&2, Nat, List.range(n)) == n : Nat}