proposition: Lemma tilt_inj (i j : 'I_k) : injective (tilt i j).
proof: Proof. by apply bij_inj; apply tilt_bij. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq path) mathcomp(ssralg fintype perm choice finfun) mathcomp(matrix bigop zmodp mxalgebra fingroup) minor