pub proof fn lemma_nat_range_finite(l: nat, r: nat)Expand description
requires
l <= r,Set::<nat>::range(l, r).len() == (r - l) as nat,The length of a set of natural numbers between l and r equals r - l.