proposition: Lemma L3toolE0 m (c: 'cV[R]_m) d : L3tool c d 0 = d.
proof: Proof. by rewrite /L3tool; case: splitP. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq path) mathcomp(ssralg fintype perm choice) mathcomp(matrix bigop zmodp mxalgebra poly polydiv mxpoly) ssrcomplements dvdring minor atomic_operations