proposition: Lemma find_lbound: forall {A:Type} {EA: EquivDec.EqDec A eq} (l: list A) v ans, ans <= find l v ans.
proof: Proof. induction l; intros. simpl. lia. simpl. destruct (EA a v). lia. rewrite find_accum_add1. specialize IHl with v ans; lia. Qed.
imports: VST.floyd.proofauto Coq.Classes.Equivalence CertiGraph.lib.List_ext