proposition: Fact phi_simpl a n p q : 0 < n -> a + (n + p) * 2 ^ q - 2 ^ q = a + (n.-1 + p) * 2 ^ q.
proof: Proof. case: n => // n _. rewrite -addnBA; last by rewrite addSn mulSn leq_addr. by rewrite [_ + p]addSn mulSn [2 ^ _ + _]addnC addnK. Qed.
imports: mathcomp(all_ssreflect) hanoi(triangular)