proposition: Lemma psi_sint3 : psi `[3] = 4.
proof: Proof. rewrite /psi psi_auxb_sint. rewrite -(big_mkord xpredT (fun l => rnz (psi_aux l _))). pose f l := rnz (((2 ^ l).-1 + \sum_(0 <= i < 3) 2 ^ minn (∇i) l)%:R - (l * 2 ^ l)%:R). rewrite (eq_bigr f) => [|i _]; last by rewrite psi_aux_sintE. by rewrite /f /= unlock. Qed.
imports: mathcomp(all_ssreflect all_algebra finmap) hanoi(extra triangular phi)