proposition: Lemma build_star_destruct_left x n sx sn: prop_star_destruct_left sx -> prop_star_destruct_left sn -> prop_star_destruct_left (@star_build x n sx sn).
proof: Proof. intros Hx Hn m M Y H. unfold star_build. set (a := mx_sub00 M). set (b := mx_sub01 M). set (c := mx_sub10 M). set (d := mx_sub11 M). set (e := sn d). set (be:= b*e). set (ec:= e*c). set (g := a + be*c). set (f := sx g). set (fbe := f*be). set (ecf := ec*f). rewrite (mx_decompose_blocks M) in H. fold a in H; fold b in H; fold c in H; fold d in H. clearbody a b c d. clear M. rewrite -> decomp_dot_leq_left in H. destruct H as (H30&H31&H32&H33). set (z := mx_sub01 (y:=0) Y) in *. set (y := mx_sub11 (y:=0) Y) in *. rewrite -> decomp_dot_leq_left. fold z; fold y. clearbody y z. clear Y. assert (H34: e*y <== y). unfold e. apply Hn, H33. clear H33. assert (H36: b*e*y <== z). monoid_rewrite H34. exact H31. clear H31. assert (H39: (a+b*e*c)*z <== z). rewrite dot_distr_left; apply plus_destruct_leq; trivial. monoid_rewrite H32. exact H36. clear H30. assert (H40: f*z <== z). unfold f. apply Hx, H39. clear H39. assert (H42: f*b*e*y <== z). monoid_rewrite H36. exact H40. assert (H45: e*c*f*z <== y). monoid_rewrite H40. monoid_rewrite H32. exact H34. clear H32. assert (H47: e*c*f*b*e*y <== y). monoid_rewrite H36. exact H45. clear H36. repeat split. exact H40. rewrite <- H42. unfold fbe, be. semiring_reflexivity. exact H45. clear H40 H42 H45. unfold ecf, ec, be. semiring_normalize; apply plus_destruct_leq. exact H34. exact H47. Qed.
imports: ATBR(Common) ATBR(Classes) ATBR(Graph) ATBR(Monoid) ATBR(SemiLattice) ATBR(SemiRing) ATBR(KleeneAlgebra) ATBR(MxGraph) ATBR(MxSemiLattice) ATBR(MxSemiRing)