proposition: Lemma psi_aux0_sint n : psi_aux 0 `[n] = n.
proof: Proof. rewrite /psi_aux add0n subr0. apply/eqP; rewrite -natz eqr_nat; apply/eqP. rewrite (eq_bigr (fun => 1)) => [|i _]. by rewrite fsum_nat_const card_sint // subn0 muln1. by rewrite minn0. Qed.
imports: mathcomp(all_ssreflect all_algebra finmap) hanoi(extra triangular phi)