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