proposition: Theorem list_fold_right_seq : ∀ g h la lb s t len, lap_eq la lb → (∀ x y z, lap_eq y z → lap_eq (g x y) (g x z)) → (∀ i accu, lap_eq (g (s + i)%nat accu) (h (t + i)%nat accu)) → lap_eq (List.fold_right g la (List.seq s len)) (List.fold_right h lb (List.seq t len)).
proof: Proof. intros g h la lb s t len Hab Hg Hgh. revert g h la lb s t Hab Hg Hgh. induction len; intros; [ assumption | simpl ]. pose proof (Hgh O (List.fold_right h lb (List.seq (S t) len))) as H. do 2 rewrite Nat.add_0_r in H. rewrite <- H. apply Hg. apply IHlen; [ assumption | assumption | idtac ]. intros i accu. do 2 rewrite Nat.add_succ_l, <- Nat.add_succ_r. apply Hgh. Qed.
imports: Utf8 QArith NPeano Misc Field2 Fsummation