[STATEMENT]
lemma nu_iso: "x \<le> y \<Longrightarrow> \<nu> x \<le> \<nu> y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<le> y \<Longrightarrow> \<nu> x \<le> \<nu> y
[PROOF STEP]
using local.inf_mono nu_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?a \<le> ?c; ?b \<le> ?d\<rbrakk> \<Longrightarrow> ?a \<sqinter> ?b \<le> ?c \<sqinter> ?d
\<nu> ?x = ?x \<sqinter> nc

goal (1 subgoal):
 1. x \<le> y \<Longrightarrow> \<nu> x \<le> \<nu> y
[PROOF STEP]
by auto