proposition: Lemma lift_diff_ord_max n (i : 'I_n.+2) : i != ord_max -> lift ord_max (inord i) = i.
proof: Proof. move=> iDm. apply/val_eqP; rewrite [val (lift _ _)]lift_max /= ?inordK //. by apply: ltn_diff_ord_max. Qed.
imports: mathcomp(all_ssreflect all_algebra finmap) hanoi(extra triangular phi)