Function vstd::seq_lib::lemma_min_of_concat

source · 
pub proof fn lemma_min_of_concat(x: Seq<int>, y: Seq<int>)
Expand description
requires
0 < x.len() && 0 < y.len(),
ensures
(x + y).min() <= x.min(),
(x + y).min() <= y.min(),
forall |elt: int| (x + y).contains(elt) ==> (x + y).min() <= elt,

The minimum of the concatenation of two non-empty sequences is less than or equal to the minimum of its two non-empty subsequences.