proposition: Lemma psi_auxE_le l e : psi_aux l e = (((2 ^ l * #|`[fset i in e | (l <= troot i)%nat]|.+1).-1 + (\sum_(i <- e | (troot i < l)%nat) 2 ^ troot i))%:R - (l * 2 ^ l)%:R)%R.
proof: Proof. rewrite /psi_aux. congr (_%:R - _%:R)%R. rewrite (big_fsetID _ [pred i | l <= ∇i]) /=. rewrite (@eq_fbigr _ _ _ _ _ _ _ (fun i => 2 ^ l)) /=; last first. by move=> i; rewrite !inE => /andP[_ /minn_idPr->]. rewrite fsum_nat_const. rewrite (@eq_fbigr _ _ _ _ _ _ _ (fun i => 2 ^ (troot i))) /=; last first. move=> i; rewrite !inE => /andP[_ H] _. suff /minn_idPl-> : troot i <= l by []. by rewrite ltnW // ltnNge. rewrite addnA; congr (_ + _)%nat. rewrite mulnS [_ ^ _ * #|`_|]mulnC. by case: (2 ^ l) (expn_gt0 2 l). by apply: eq_fbigl_cond => i; rewrite !inE ltnNge andbT. Qed.
imports: mathcomp(all_ssreflect all_algebra finmap) hanoi(extra triangular phi)