proposition: Lemma mx_sup `{X: lattice.ops} n m I J (f: I -> mx X n m) i j: (\sup_(x\in J) f x) i j = \sup_(x\in J) f x i j.
proof: Proof. apply (f_sup_eq (fun x: mx X n m => x i j)); now f_equal. Qed.
imports: comparisons kleene sums normalisation