proposition: Lemma psum_exten n f g : (forall k, k < n -> f k = g k) -> (psum f n).+1 = (psum g n).+1.
proof: Proof. move => h; rewrite /psum; congr S; apply: eq_big => // [] [i lin] _ /=. by apply: h. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)