proposition: Lemma build_star_make_left x n sx sn: prop_star_make_left sx -> prop_star_make_left sn -> prop_star_make_left (@star_build x n sx sn).
proof: Proof. intros Hx Hn M. 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). setoid_rewrite (mx_decompose_blocks M). fold a; fold b; fold c; fold d. clearbody a b c d. clear M. rewrite mx_blocks_one, mx_blocks_dot, mx_blocks_plus. apply mx_blocks_compat. unfold fbe, f. rewrite <- dot_assoc, <- dot_distr_right. apply Hx. unfold fbe, be. transitivity ((f*b)*(1+e*d)). clear - KA. semiring_reflexivity. unfold e. clearbody f. rewrite (Hn d). semiring_reflexivity. unfold ecf, ec, be. transitivity ((e*c)*(1+f*(a+b*e*c))). clear - KA. semiring_reflexivity. unfold f. clearbody f. rewrite <- (Hx g) at 2. reflexivity. unfold ecf, ec, be. transitivity ((1+e*c*f*b)*(1+e*d)). clearbody e f. clear - KA. semiring_reflexivity. unfold e. clearbody e. rewrite (Hn d). semiring_reflexivity. Qed.
imports: ATBR(Common) ATBR(Classes) ATBR(Graph) ATBR(Monoid) ATBR(SemiLattice) ATBR(SemiRing) ATBR(KleeneAlgebra) ATBR(MxGraph) ATBR(MxSemiLattice) ATBR(MxSemiRing)