proposition: Lemma psi_sint_leq a b : a <= b -> psi `[a] <= psi `[b].
proof: Proof. move=> aLb; apply: psi_sub; apply/fsubsetP=> i. by rewrite !mem_sint /= => iLa; apply: leq_trans aLb. Qed.
imports: mathcomp(all_ssreflect all_algebra finmap) hanoi(extra triangular phi)