proposition: Lemma bounded_lookup f (k:nat) m : {i | i < m /\ f i = k} + ~ exists i, i < m /\ f i = k.
proof: Proof. induction m. now right; intros [i [L _]]; inversion L. destruct IHm as [[i Hi]|N]. now left; exists i; lia. assert (D:{f m = k} + {f m <> k}) by eauto with *. destruct D. now subst; eauto. right; intros [i Hi]. assert (D:i = m \/ i < m) by lia; intuition eauto. now subst; eauto. Defined.
imports: Lia