proposition: Lemma psi_eq0 e : (psi e == 0) = (e == fset0).
proof: Proof. have [->|[x]] := fset_0Vmem e; first by rewrite psi_set0 !eqxx. have [->|_] := e =P fset0; first by rewrite inE. move=> xIe. suff : psi e > 0 by case: psi. rewrite -(ltr_nat (Num.NumDomain.clone _ int)). apply: lt_le_trans (psi_max _ 0). by rewrite /psi_aux add0n subr0 ltr_nat (big_fsetD1 x). Qed.
imports: mathcomp(all_ssreflect all_algebra finmap) hanoi(extra triangular phi)