proposition: Lemma psi_set0 : psi fset0 = 0.
proof: Proof. rewrite /psi psi_auxb_set0. rewrite !big_ord_recr /= big_ord0 /= max0n. by rewrite /psi_aux /= big_seq_cond big1. Qed.
imports: mathcomp(all_ssreflect all_algebra finmap) hanoi(extra triangular phi)