proposition: Lemma mx_str_ind' (P: forall n, mx (X u u) n n -> mx (X u u) n n -> Prop): (forall n, Proper (weq ==> weq ==> iff) (P n)) -> (forall M, P O M M) -> (forall M, P _ M (scal_mx ((mx_scal M)^*))) -> (forall n m a b c d, let e := d^* in let be := b⋅e in let ec := e⋅c in let f := (a+be⋅c)^* in let fbe := f⋅be in let ecf := ec⋅f in P m d e -> P n (a+be⋅c) f -> P _ (blk_mx a b c d) (blk_mx f fbe ecf (e+ecf⋅be))) -> forall n M, P n M (M^*).
proof: Proof. intros HP HO H1 Hplus. apply (mx_str_ind P HP HO H1). intros n m Hn Hm M. rewrite (to_blk_mx M) at 1. now apply Hplus. Qed.
imports: kleene normalisation ordinal sups matrix