proposition: Lemma fold_left_permut : forall {A} f (acc : A) p q, (forall u v w, f (f u v) w = f (f u w) v) -> permut p q -> fold_left f p acc = fold_left f q acc.
proof: Proof. intros A f acc p q Hf Hpq. rewrite <- 2!fold_left_rev_right. apply fold_right_permut. now intros u v w. apply permut_trans with p. apply permut_rev. apply permut_trans with (1 := Hpq). apply permut_sym, permut_rev. Qed.
imports: Coq(List Arith ZArith Psatz) mathcomp.ssreflect(ssrfun ssrbool fintype)