proposition: Lemma psi_sint_min n : n <= psi `[n].
proof: Proof. rewrite -(ler_nat (Num.NumDomain.clone _ int)). rewrite natz -[X in (X <= _)%R]psi_aux0_sint. by apply: psi_max. Qed.
imports: mathcomp(all_ssreflect all_algebra finmap) hanoi(extra triangular phi)