proposition: Lemma sumr_add : forall (R : ringType) m n (F : 'I_(m + n) -> R), \sum_(i < m + n) F i = \sum_(i < m) F (lshift _ i) + \sum_(i < n) F (rshift _ i).
proof: Proof. move=> R; elim=> [|m ihm] n F. rewrite !big_ord0 add0r; apply: congr_big=> // [[i hi]] _. by rewrite /rshift /=; congr F; apply: val_inj. rewrite !big_ord_recl ihm -addrA. congr (_ + _); first by congr F; apply: val_inj. congr (_ + _); by apply: congr_big=> // i _ /=; congr F; apply: val_inj. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq choice fintype) mathcomp(bigop ssralg matrix zmodp div)