proposition: Lemma phi_le m n : m <= n -> phi m <= phi n.
proof: Proof. elim: n m => [[] //|n IH m]. rewrite leq_eqVlt => /orP[/eqP->//|/IH /leq_trans->//]. by rewrite phiS leq_addr. Qed.
imports: mathcomp(all_ssreflect) hanoi(triangular)