proposition: Lemma mx_scal_str `{laws} `{BKA ≪ l} u (M: mx (X u u) 1 1): mx_scal (M^*) ≡ (mx_scal M)^*.
proof: Proof. apply str_weq. unfold mx_scal, sub00_mx, tsub_mx, lsub_mx. simpl. setoid_rewrite ord0_unique. apply cupxb. Qed.
imports: kleene normalisation ordinal sups matrix