proposition: Lemma mx_str_ind_l n m (M: mx n n) (N: mx n m): M ⋅ N ≦ N -> mx_str _ _ _ M ⋅ N ≦ N.
proof: Proof. revert m N. induction n. intros ? ? _ i; elim (ord_0_empty i). simpl mx_str. apply (mx_str_build_ind_l 1); trivial. clear M IHn. intros M p N H i j. simpl. unfold mx_dot, scal_mx. simpl. setoid_rewrite ord0_unique. rewrite cupxb. apply str_ind_l. rewrite <-(H ord0 j) at 2. apply weq_geq. apply cupxb. Qed.
imports: comparisons kleene sums normalisation