proposition: Lemma mx_str_diagonal n1 n2 (a: mx (X u u) n1 n1) (d: mx (X u u) n2 n2): (blk_mx a 0 0 d)^* ≡ blk_mx (a^*) 0 0 (d^*).
proof: Proof. rewrite mx_str_trigonal. apply blk_mx_weq; trivial; ra. Qed.
imports: kleene normalisation ordinal sups matrix