proposition: Lemma fold_left_right_assoc_eq {A B} {f: A -> B -> A} (assoc: forall a b c, f (f a b) c = f (f a c) b) {n} (v: t B n): forall a, fold_left f a v = fold_right (fun x y => f y x) v a.
proof: Proof. assert (forall n h (v: t B n) a, fold_left f (f a h) v = f (fold_left f a v) h). - intros n0 h v0; induction v0 as [|? ? v0 IHv0]. + now simpl. + intros; simpl. rewrite<- IHv0, assoc. now f_equal. - induction v as [|? ? v IHv]. + reflexivity. + simpl. intros; now rewrite<- (IHv). Qed.
imports: VectorDef PeanoNat Eqdep_dec