Imports
CLRS Section 26.2 — Parallel Matrix Algorithms
This navigation module groups the executable P-ADD and P-MATMUL
definitions with their value-correctness theorems and exact execution-attached
work/span equalities and all-input asymptotic main theorems.