proposition: Lemma invset_eltrR s (i : 'I_n) : i < n0 -> s^-1 i < s^-1 (inord i.+1) -> invset (s * 's_i) = (s^-1 i, s^-1 (inord i.+1)) |: invset s.
proof: Proof. move=> Hi Hfwd. rewrite -eltrV -{1}(invgK s) -invMg invset_permV. rewrite invset_eltrL // imsetU1; congr (_ |: _). - by rewrite /= !permM eltrL eltrR. - rewrite invset_permV -!imset_comp -[RHS](imset_id) /=; apply eq_imset. by move=> [u v]; rewrite /= !permM !eltrK !permK. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(fingroup perm morphism presentation) mathcomp(ssralg poly ssrint) permcomp tools permuted combclass congr