proposition: Lemma phi_odd n : odd (phi n) = (0 < n).
proof: Proof. case: n => // [] [|n] //. rewrite phi_modSE oddD oddM oddX orbF. case: troot (troot_gt0 (isT : 0 < n.+1)) => // k. by rewrite andbF. Qed.
imports: mathcomp(all_ssreflect) hanoi(triangular)