proposition: Lemma big_fsetD1cond (a : I) (A : {fset I}) (P : pred I) (F : I -> R) : a \in A -> P a -> \big[op/idx]_(i <- A | P i) F i = op (F a) (\big[op/idx]_(i <- A `\ a | P i) F i).
proof: Proof. move=> aA aP; rewrite (big_fsetIDcond _ (mem [fset a])). congr (op _ _); last first. by apply: eq_fbigl_cond => i; rewrite !inE /= [_ && (_ != _)]andbC. rewrite (_ : [fset _ | _ in _ & _] = [fset a]). rewrite big_seq_fsetE /= /index_enum /= -enumT enum_fset1 /=. by rewrite unlock /= aP Monoid.Theory.mulm1. by apply/fsetP=> i; rewrite !inE /= andbC; case: eqP => //->. Qed.
imports: mathcomp(all_ssreflect all_algebra finmap) hanoi(extra triangular phi)