proposition: Lemma ltn_diff_ord_max n (i : 'I_n.+2) : i != ord_max -> i < n.+1.
proof: Proof. move/eqP/val_eqP. by have := ltn_ord i; rewrite ltnS leq_eqVlt => /orP[->|]. Qed.
imports: mathcomp(all_ssreflect all_algebra finmap) hanoi(extra triangular phi)