proposition: Lemma build_star_destruct_right x n sx sn: prop_star_destruct_right sx -> prop_star_destruct_right sn -> prop_star_destruct_right (@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_right in H. destruct H as (H30&H31&H32&H33). set (y := mx_sub10 (x:=0) Y)in*. set (z := mx_sub11 (x:=0) Y)in*. rewrite -> decomp_dot_leq_right. fold z; fold y. clearbody y z. clear Y. assert (H34: z*e <== z). unfold e. apply Hn, H33. clear H33. assert (H35: z*e*c <== z*c). monoid_rewrite H34. reflexivity. assert (H36: z*e*c<== y). rewrite <- H31. trivial. assert (H39: y*(a+b*e*c) <== y). rewrite dot_distr_right; apply plus_destruct_leq; trivial. rewrite 2dot_assoc, H32. exact H36. assert (H40: y*f <== y). unfold f. apply Hx, H39. assert (H42: z*e*c*f <== y). rewrite H36. exact H40. assert (H45: y*f*b*e <== z). rewrite H40. rewrite H32. exact H34. assert (H46: z*e*c*f*b*e <== y*f*b*e). rewrite H36. reflexivity. assert (H47: z*e*c*f*b*e <==z). rewrite <- H45 at 2. exact H46. clear - KA H40 H42 H45 H34 H47. repeat split. exact H40. rewrite <- H42. unfold ecf, ec. semiring_reflexivity. unfold fbe, be. semiring_normalize. exact H45. semiring_normalize; apply plus_destruct_leq. unfold ecf, ec, be. semiring_normalize. exact H47. exact H34. Qed.
imports: ATBR(Common) ATBR(Classes) ATBR(Graph) ATBR(Monoid) ATBR(SemiLattice) ATBR(SemiRing) ATBR(KleeneAlgebra) ATBR(MxGraph) ATBR(MxSemiLattice) ATBR(MxSemiRing)