proposition: Lemma mx_str_build_ind_r: transfers (fun n M sM => forall p (N: mx p n), N⋅M ≦ N -> N⋅sM ≦ N).
proof: Proof. intros Hf He M p N. rewrite (to_blk_mx M) at 1. unfold_s M. rewrite (to_row_mx N). set (h := lsub_mx N). set (k:= rsub_mx N). specialize (Hf (a+b⋅e⋅c) p h). specialize (He d p k). fold e in He. fold f in Hf. clearbody a b c d e f h k. clear - He Hf L Hl. unfold blk_mx. rewrite 2mx_dot_rowcol, 4mx_dot_xrow. setoid_rewrite <-row_mx_cup. setoid_rewrite row_mx_leq_iff. rewrite 2cup_spec. intros [[Ha Hb] [Hc Hd]]. specialize (He Hd). revert Hf. rewrite 2dotxpls, 4cup_spec, !dotA. intro Hf. apply apply in Hf; repeat split; repeat (trivial; rewrite ?Ha, ?Hb, ?Hc, ?Hd, ?He, ?Hf). Qed.
imports: comparisons kleene sums normalisation