pub proof fn lemma_first_zero_index_is_first_zero(s: Seq<bool>)Expand description
ensures
is_first_zero(s, first_zero_index(s)),first_zero_index(s) itself satisfies is_first_zero (induction on s.len()).