Idris package defining, implementing, and verifying naiive Gaussian elimination over the integers in some system of linear algebra.