proposition: Lemma psi_aux_sub l e1 e2 : e1 `<=` e2 -> (psi_aux l e1 <= psi_aux l e2)%R.
proof: Proof. move=> e1Se2. apply: lerB => //. rewrite ler_nat. rewrite leq_add2l //. rewrite [X in _ <= X](bigID (fun i => i \in e1)) /=. suff iH : [fset x in e1 | xpredT x] =i [fset i in e2 | i \in e1]. by rewrite (eq_fbigl_cond _ _ iH) /= leq_addr. move=> i; rewrite !inE /=. have /fsubsetP/(_ i) := e1Se2. by case: (i \in e1) => [->//|]; rewrite andbF. Qed.
imports: mathcomp(all_ssreflect all_algebra finmap) hanoi(extra triangular phi)