proposition: Lemma mx_dot_kfun1 `{laws} `{BSL ≪ l} u n m i p (M: mx (X u u) m p): (mx_fun (n:=n) (fun _ => i) 1 ⋅ M) ≡ fun _ j => M i j.
proof: Proof. intros j k. rewrite mx_dot_fun. apply dot1x. Qed.
imports: kleene normalisation ordinal sups matrix