proposition: Lemma find_range_gen: forall (l: list Z) target ans, In target l -> 0 <= ans -> ans <= find l target ans < Zlength l + ans.
proof: Proof. intros. generalize dependent target. generalize dependent ans. induction l. 1: intros; simpl; now rewrite Zlength_nil. intros. apply in_inv in H. destruct H. - subst a. unfold find. destruct (Z_EqDec target target). rewrite Zlength_cons. split; rep_lia. exfalso. apply c. reflexivity. - unfold find. destruct (Z_EqDec a target). 1: rewrite Zlength_cons; split; rep_lia. assert (0 <= 1 + ans) by lia. pose proof (IHl (1+ans) H1 target H). clear -H2. unfold find in H2. rewrite Zlength_cons. rep_lia. Qed.
imports: VST.floyd.proofauto Coq.Classes.Equivalence CertiGraph.lib.List_ext