proposition: Lemma phi_leD a b : phi (a + b) <= (phi a).*2 + (2 ^ b).-1.
proof: Proof. case: b => [|b]; first by rewrite !addn0 -addnn leq_addr. rewrite phi_gmin -{3}[b.+1](addnK a _) [b.+1 + a]addnC. apply: gmin_min. by rewrite -addSnnS leq_addr. Qed.
imports: mathcomp(all_ssreflect) hanoi(triangular)