proposition: Lemma mx_blocks_dot n m n' m' p p': forall (a : MX n m ) (b : MX n m') (c : MX n' m ) (d : MX n' m') (a': MX m p ) (b': MX m p') (c': MX m' p ) (d': MX m' p'), mx_blocks a b c d * mx_blocks a' b' c' d' == mx_blocks (a * a' + b * c') (a * b' + b * d') (c * a' + d * c') (c * b' + d * d').
proof: Proof. simpl. intros. destruct_blocks. rewrite (Nat.add_comm m), sum_cut. apply plus_compat. apply sum_compat; intros. destruct_blocks. reflexivity. lia_false. rewrite (Nat.add_comm m), sum_shift. apply sum_compat; intros. destruct_blocks. reflexivity. rewrite (Nat.add_comm m), sum_cut. apply plus_compat. apply sum_compat; intros. destruct_blocks. reflexivity. lia_false. rewrite (Nat.add_comm m), sum_shift. apply sum_compat; intros. destruct_blocks. reflexivity. rewrite (Nat.add_comm m), sum_cut. apply plus_compat. apply sum_compat; intros. destruct_blocks. reflexivity. lia_false. rewrite (Nat.add_comm m), sum_shift. apply sum_compat; intros. destruct_blocks. reflexivity. rewrite (Nat.add_comm m), sum_cut. apply plus_compat. apply sum_compat; intros. destruct_blocks. reflexivity. lia_false. rewrite (Nat.add_comm m), sum_shift. apply sum_compat; intros. destruct_blocks. reflexivity. Qed.
imports: ATBR(Common) ATBR(Classes) ATBR(Graph) ATBR(Monoid) ATBR(SemiLattice) ATBR(SemiRing) ATBR(MxGraph) ATBR(MxSemiLattice) ATBR(BoolView)