proposition: Lemma mx_str_1 (M: mx (X u u) 1 1): M^* ≡ scal_mx ((mx_scal M)^*).
proof: Proof. intros i j. setoid_rewrite ord0_unique. simpl. unfold mx_str_build, blk_mx, col_mx, row_mx, ordinal.split; simpl. unfold mx_scal, scal_mx, mx_dot, sub00_mx, tsub_mx, lsub_mx; simpl. setoid_rewrite ord0_unique. ra. Qed.
imports: kleene normalisation ordinal sups matrix