proposition: Lemma set_ord_max_lift n (e : {set 'I_n.+2}) : e :\ ord_max = [set lift ord_max x | x in [set i | lift ord_max i \in e]].
proof: Proof. apply/setP => i; rewrite !inE /=. apply/andP/imsetP => [[iH iIe]|[j //]]. exists (inord i). by rewrite inE lift_diff_ord_max. by rewrite lift_diff_ord_max. rewrite inE => kH ->; split => //. apply/eqP/val_eqP. by rewrite [val (lift _ _)]lift_max /= neq_ltn ltn_ord. Qed.
imports: mathcomp(all_ssreflect all_algebra finmap) hanoi(extra triangular phi)