proposition: Lemma tiltK (i j: 'I_k) : involutive (tilt i j).
proof: Proof. by move => s; apply/permP => x; rewrite !permM tpermK. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq path) mathcomp(ssralg fintype perm choice finfun) mathcomp(matrix bigop zmodp mxalgebra fingroup) minor