proposition: Lemma phi_3_5_4_sum n : phi (n.+3) = (\sum_(1 <= i < n.+3) 2 ^ troot i).+1.
proof: Proof. rewrite phiE. rewrite -(big_mkord xpredT (fun i => 2 ^ troot i)). rewrite (big_cat_nat _ _ _ (_ : 0 <= 1)) //=. by rewrite big_nat_recl //= big_mkord big_ord0 addn0 add1n. Qed.
imports: mathcomp(all_ssreflect all_algebra finmap) hanoi(extra triangular phi)