proposition: Lemma psi_sintS n : (psi `[n.+1] = psi `[n] + 2 ^ (troot n.+1).-1)%nat.
proof: Proof. have F : 0 < phi n.+1 by apply: phi_le (_ : 1 <= _). apply: double_inj; rewrite doubleD. rewrite !psi_sint_phi //. rewrite -mul2n -expnS prednK ?troot_gt0 //. by rewrite phiE big_ord_recr -phiE prednDl. Qed.
imports: mathcomp(all_ssreflect all_algebra finmap) hanoi(extra triangular phi)