proposition: Lemma decomp_dot_leq_left x n m (a: SMX x) b c (d: SMX n) (Y: MX (x+n) m): mx_blocks a b c d * Y <== Y <-> let z := mx_sub01 (y:=0) Y in let y := mx_sub11 (y:=0) Y in a*z <== z /\ b*y <== z /\ c*z <== y /\ d*y <== y.
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 (_&H1&_&H2). destruct (leq_destruct_plus H1) as [H11 H12]; clear H1. destruct (leq_destruct_plus H2) as [H21 H22]; clear H2. 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)