Function lemma_first_zero_index_after_true_prefix 

pub proof fn lemma_first_zero_index_after_true_prefix(s: Seq<bool>, k: int)

requires

0 <= k <= s.len(),

forall |j: int| 0 <= j < k ==> s[j],

ensures

first_zero_index(s) == k + first_zero_index(s[k..]),

If the prefix [0, k) of s is all true, then the first zero of s is k plus the first zero of the remainder (induction on s.len()).