proposition: Lemma mx_dot_fun `{laws} `{BSL ≪ l} u n m f z p (M: mx (X u u) m p) i j: (mx_fun (n:=n) f z ⋅ M) i j ≡ z ⋅ M (f i) j.
proof: Proof. simpl. unfold mx_dot. apply antisym. apply leq_supx. intros j' _. unfold mx_fun. case eqb_ord_spec. intros ->. ra. intros _. ra. rewrite <- (leq_xsup _ _ (f i)). 2: apply in_seq. unfold mx_fun. now rewrite eqb_refl. Qed.
imports: kleene normalisation ordinal sups matrix