proposition: Lemma phiE n : phi n = \sum_(i < n) 2 ^ troot i.
proof: Proof. rewrite -(@big_mkord _ _ _ _ predT (fun i => 2 ^ (troot i))). rewrite unlock /reducebig /phi. by rewrite /index_iota subn0. Qed.
imports: mathcomp(all_ssreflect) hanoi(triangular)