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