proposition: Lemma fold_left_Zadd_comp: forall (l1 l2: list Z), Zlength l1 = Zlength l2 -> (forall i, 0<=i<Zlength l1 -> Znth i l1 <= Znth i l2) -> (forall s, fold_left Z.add l1 s <= fold_left Z.add l2 s).
proof: Proof. induction l1; intros. rewrite Zlength_nil in H. symmetry in H. apply Zlength_nil_inv in H. subst l2. lia. destruct l2. rewrite Zlength_cons in H. rewrite Zlength_nil in H. pose proof (Zlength_nonneg l1). lia. simpl. assert (a <= z). replace a with (Znth 0 (a::l1)). replace z with (Znth 0 (z::l2)). apply H0. split. lia. rewrite Zlength_cons. pose proof (Zlength_nonneg l1). lia. auto. auto. apply (Z.le_trans _ (fold_left Z.add l1 (s + z)) _). apply fold_left_Zadd_diff_accum. lia. apply IHl1. do 2 rewrite Zlength_cons in H. lia. intros. replace (Znth i l1) with (Znth (i+1) (a::l1)). replace (Znth i l2) with (Znth (i+1) (z::l2)). apply H0. rewrite Zlength_cons. lia. all: rewrite (Znth_pos_cons (i+1)) by lia; rewrite Z.add_simpl_r; auto. Qed.
imports: Coq.Lists.List Coq.micromega.Lia Coq.Sorting.Permutation Coq.ZArith.ZArith_base Coq.ZArith.Zcomplements Coq.Logic.FunctionalExtensionality CertiGraph.lib.Coqlib CertiGraph.lib.EquivDec_ext VST.zlist.sublist VST.zlist.list_solver