proposition: Lemma shiftinv_posK pos i : i != pos -> shift_pos pos (shiftinv_pos pos i) = i.
proof: Proof. Proof using. rewrite /shift_pos /shiftinv_pos => Hipos. case (ltnP i pos) => [-> // | Hi]. case: i Hipos Hi => [| i] /=. - move=> H1 H2; exfalso. move: H2; rewrite leqn0 => /eqP H. by rewrite H in H1. - rewrite ltnNge => H1 H2. rewrite eq_sym in H1. by rewrite -ltnS ltn_neqAle H1 H2 /=. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(order) tools