proposition: Lemma fold_right_permut : forall {A} f (acc : A) p q, (forall u v w, f u (f v w) = f v (f u w)) -> permut p q -> fold_right f acc p = fold_right f acc q.
proof: Proof. intros A f acc p q Hf. revert acc q. induction p as [|h p IH] ; intros acc. intros [|q]. easy. intros [Hl _ _ _]. easy. intros q Hq. apply permut_remove in Hq. destruct Hq as [s [t [H1 H2]]]. simpl. rewrite IH with (1 := H2). rewrite H1. clear -Hf. induction s as [|k s IH]. easy. simpl. now rewrite <- IH. Qed.
imports: Coq(List Arith ZArith Psatz) mathcomp.ssreflect(ssrfun ssrbool fintype)