proposition: Lemma psiE e : {l | ((psi e)%:R = psi_aux l e)%R}.
proof: Proof. have [l] : {l : 'I_(psi_auxb e) | psi e = rnz (psi_aux l e)}. apply bigop.eq_bigmax. by rewrite card_ord. rewrite /rnz; case: ler0P => [pG pE|pP ->]; last first. by exists l; rewrite natz gtz0_abs. by exists 0; apply/eqP; rewrite eq_le {1}pE psi_aux_0_ge0 psi_max. Qed.
imports: mathcomp(all_ssreflect all_algebra finmap) hanoi(extra triangular phi)