The usual proofs of the existence of LU-factorizations are done in terms of elementary matrices. The Maple implementation below follows the usual proofs closely (in fact, one can say that the structure of the code is a proof for the decomposition --- in particular, the loop invariants provide an inductive proof, given the properties of elementary matrices).