proposition: Lemma Znth_find_gen: forall (l: list Z) target ans, 0 <= ans -> In target l -> Znth ((find l target ans)-ans) l = target.
proof: Proof. intros. generalize dependent ans. induction l. 1: inversion H0. intros. destruct H0. - subst target. simpl. destruct (Z_EqDec a a). + replace (ans-ans) with 0 by lia. rewrite Znth_0_cons; auto. + exfalso; apply c; reflexivity. - specialize (IHl H0). simpl. destruct (Z_EqDec a target). + replace (ans-ans) with 0 by lia. rewrite Znth_0_cons; auto. + assert (0 <= 1 + ans) by lia. specialize (IHl (1+ans) H1). rewrite Znth_pos_cons. replace (1+ans) with (ans+1) in IHl at 2 by lia. rewrite Z.sub_add_distr in IHl. assumption. destruct (find_range_gen l target (1+ans) H0 H1) as [? _]. lia. Qed.
imports: VST.floyd.proofauto Coq.Classes.Equivalence CertiGraph.lib.List_ext