proposition: Lemma psi_aux_sintE n l : psi_aux l `[n] = (((2 ^ l).-1 + \sum_(0 <= i < n) 2 ^ minn (∇i) l)%:R - (l * 2 ^ l)%:R)%R.
proof: Proof. congr ((_ + _)%:R - _%:R)%R. elim: n => [|n IH]; first by rewrite sint0_set0 /= big_nil. rewrite (big_fsetD1 n) /=; last by rewrite mem_sint andTb. by rewrite sintSr IH !big_mkord big_ord_recr /= addnC. Qed.
imports: mathcomp(all_ssreflect all_algebra finmap) hanoi(extra triangular phi)