proposition: Lemma psiE_leq e n : psi_auxb e <= n -> psi e = \max_(l < n) rnz (psi_aux l e).
proof: Proof. move=> pLn. rewrite /psi. rewrite (big_ord_widen_cond _ xpredT (fun i => rnz (psi_aux i e)) pLn). rewrite [RHS](bigID (fun i : 'I_n => i < psi_auxb e)) /=. rewrite [X in _ = maxn _ X]big1 ?maxn0 // => i. rewrite -leqNgt => /psi_aux_psib. exact: rnz_ler0. Qed.
imports: mathcomp(all_ssreflect all_algebra finmap) hanoi(extra triangular phi)