lemma_nat_range_finite

vstd_extra::set_extra

Function lemma_nat_range_finite 

Source 
pub proof fn lemma_nat_range_finite(l: nat, r: nat)
Expand description
requires
l <= r,
ensures
Set::new(|p: nat| l <= p < r).finite(),
Set::new(|p: nat| l <= p < r).len() == (r - l) as nat,

If all elements of set s are natural numbers between l and r, then the set is finite.