Function vstd::seq_lib::lemma_max_of_concat
source · pub proof fn lemma_max_of_concat(x: Seq<int>, y: Seq<int>)Expand description
requires
0 < x.len() && 0 < y.len(),x.max() <= (x + y).max(),y.max() <= (x + y).max(),forall |elt: int| (x + y).contains(elt) ==> elt <= (x + y).max(),The maximum of the concatenation of two non-empty sequences is greater than or equal to the maxima of its two non-empty subsequences.