proposition: Lemma psi_auxb_sint n : psi_auxb `[n] = n.+1.
proof: Proof. congr (_.+1). rewrite /psi_auxb. rewrite card_sint ?geq_minr // subn0. apply/eqP. rewrite eqn_leq leq_maxl andbT geq_max leqnn andTb. apply/bigfmax_leqP => i; rewrite mem_sint /= => iLn _. by apply: leq_trans (leq_rootnn _) (ltnW _). Qed.
imports: mathcomp(all_ssreflect all_algebra finmap) hanoi(extra triangular phi)