proposition: Lemma find_range: forall l target, In target l -> 0 <= find l target 0 < Zlength l.
proof: Proof. intros. replace (Zlength l) with (Zlength l + 0) by lia. apply find_range_gen; trivial; lia. Qed.
imports: VST.floyd.proofauto Coq.Classes.Equivalence CertiGraph.lib.List_ext