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