proposition: Lemma mx_str_unfold_l n (M: mx n n): 1 + M ⋅ mx_str _ _ _ M ≦ mx_str _ _ _ M.
proof: Proof. induction n. intro i; elim (ord_0_empty i). simpl mx_str. apply (mx_str_build_unfold_l 1); trivial. intros N i j. simpl. unfold mx_dot, scal_mx, mx_one. simpl. setoid_rewrite ord0_unique. simpl. now rewrite cupxb, <-str_unfold_l. Qed.
imports: comparisons kleene sums normalisation