proposition: Lemma fold_left_rev_right A B: forall (f:A->B->B) n (v : t A n) a, fold_right f (rev v) a = fold_left (fun x y => f y x) a v.
proof: Proof. intros f n v. induction v as [|b n v IH]; intros a. - now rewrite rev_nil. - rewrite rev_cons, fold_right_shiftin. apply IH. Qed.
imports: VectorDef PeanoNat Eqdep_dec