proposition: Lemma shift_posK pos i : shiftinv_pos pos (shift_pos pos i) = i.
proof: Proof. Proof using. rewrite /shift_pos /shiftinv_pos. case (ltnP i pos) => [-> // | Hi]. by rewrite ltnNge (leq_trans Hi (leqnSn _)). Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(order) tools