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, (forall M, P n M (M^*)) -> (forall M, P m M (M^*)) -> forall M, P _ M (mx_str_build _ _ n m (fun M => M^*) (fun M => M^*) M)) -> forall n M, P n M (M^*).
proof: Proof. intros HP HO H1 Hplus n M. induction n as [|n IHn]. apply HO. change (M^*) with (mx_str _ _ _ M). unfold mx_str, mx_str_build. ra_fold (mx_ops X). setoid_rewrite <-mx_str_1. revert M; refine (Hplus (S O) n _ _); intro M. rewrite mx_str_1. apply H1. apply IHn. Qed.
imports: kleene normalisation ordinal sups matrix