proposition: Lemma sum_sint (F : nat -> nat) n : \sum_(i <- `[n]) F i = \sum_(i < n) F i.
proof: Proof. rewrite big_seq_cond. rewrite [LHS](eq_bigl (fun i => (i < n))); last first. by move=> i; rewrite mem_sint andbT. rewrite [RHS](eq_bigl (fun i : 'I_ _ => ((i : nat) \in (enum_fset `[n])))); last first. by move=> i; rewrite mem_sint ltn_ord. elim: enum_fset (fset_uniq `[n]) => /= [_|a l IH /andP[aNIl lU]]. by rewrite big_nil big1. rewrite big_cons /= IH //; case: (boolP (a < n)) => aLn; last first. apply: eq_bigl => i; move: (ltn_ord i); rewrite inE; case: eqP => [->| //]. by rewrite (negPf aLn). rewrite [RHS](bigD1 (Ordinal aLn)) ?(inE, eqxx) //=. congr ((_ + _)%nat). apply: eq_bigl => i; rewrite inE -val_eqE /=. by case: (_ =P _); rewrite ?andbT // => ->; rewrite (negPf aNIl). Qed.
imports: mathcomp(all_ssreflect all_algebra finmap) hanoi(extra triangular phi)