proposition: Lemma decomp_dot_leq_right x n m (a: SMX x) b c (d: SMX n) (Y: MX m (x+n)): Y * mx_blocks a b c d <== Y <-> let y := mx_sub10 (x:= 0) Y in let z := mx_sub11 (x:= 0) (y:=x) Y in y * a <== y /\ z * c <== y /\ y * b <== z /\ z * d <== z.
proof: Proof. change m with (0+m)%nat in *. split; intro H. rewrite (mx_decompose_blocks Y) in H at 2. rewrite (mx_decompose_blocks Y) in H at 1. rewrite mx_blocks_dot in H. destruct (mx_blocks_leq H) as (H0&H1&H2&H3). destruct (leq_destruct_plus H0) as [H01 H02]; clear H0. destruct (leq_destruct_plus H1) as [H11 H12]; clear H1. destruct (leq_destruct_plus H2) as [H21 H22]; clear H2. destruct (leq_destruct_plus H3) as [H31 H32]; clear H3. repeat split; assumption. rewrite (mx_decompose_blocks Y) at 2. rewrite (mx_decompose_blocks Y) at 1. rewrite mx_blocks_dot. do 2 intuition. apply mx_blocks_incr; apply plus_destruct_leq; simpl Peano.plus in *; trivial; repeat intro; lia_false. Qed.
imports: ATBR(Common) ATBR(Classes) ATBR(Graph) ATBR(Monoid) ATBR(SemiLattice) ATBR(SemiRing) ATBR(KleeneAlgebra) ATBR(MxGraph) ATBR(MxSemiLattice) ATBR(MxSemiRing)