proposition: Lemma mx_str_build_unfold_l: transfers (fun n M sM => 1+M⋅sM ≦ sM).
proof: Proof. intros Hf He M. rewrite (to_blk_mx M) at 1. unfold_s M. specialize (Hf (a+b⋅e⋅c)). specialize (He d). fold e in He. fold f in Hf. clearbody a b c d e f. clear - He Hf L Hl. apply leq_cupx. rewrite one_blk_mx. apply blk_mx_leq; hlattice. rewrite mx_dot_blk. apply blk_mx_leq. rewrite <- Hf at 3. ra. rewrite <- Hf at 3. ra. rewrite <- He at 2. ra. rewrite <- He at 5 6. ra. Qed.
imports: comparisons kleene sums normalisation