sum.v

From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq choice path.
From mathcomp Require Import div fintype tuple finfun bigop finset fingroup perm.
From mathcomp Require Import div prime binomial ssralg finalg zmodp countalg ssrnum falgebra.
From mathcomp Require Import ssrint matrix algC.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.


Local Open Scope ring_scope.
Definition test_kernel :=
    \matrix_(i < 3%N, j < 3%N)  1%:Z.

Lemma tmp0 n (T:ringType) (f: 'I_n -> T):
    \sum_(i<n) f i = foldr (+%R) 0%R (map f (ord_enum n)).
Proof.
    rewrite !unlock /reducebig /index_enum /applybig => //=.
    rewrite !unlock /comp => //=.
    by rewrite foldr_map.
Qed.

Example tmp j:
    \sum_i (test_kernel i j) = 3.
Proof.
    rewrite  /test_kernel /test_image.
    rewrite tmp0.
    rewrite /ord_enum => //=.