pub broadcast proof fn range_set_properties<A: FiniteRange>(lo: A, hi: A)Expand description
ensures
forall |i: A| #[trigger] A::range_set(lo, hi).contains(i) <==> A::in_range(i, lo, hi),(#[trigger] A::range_set(lo, hi)).len() == A::range_len(lo, hi),This public broadcast lemma shows that when A has trait
FiniteRange, A::range_set(lo, hi) has the expected properties.
That is, it contains all values a: A such that lo <= a < hi,
and its length is hi - lo.