proposition: Lemma rsym_invsetP s : sorted (rsymrel (invset s)) [seq s^-1 i | i : 'I_n].
proof: Proof. case: (n =P 0) => [neq0 | /eqP nnon0]. suff -> : [seq s^-1 i | i : 'I_n] = [::] by []. by apply: size0nil; rewrite size_map size_enum_ord. have {nnon0} ord0 : 'I_n by case: n {s} nnon0 => // n0 _; apply ord0. apply/(sortedP ord0) => i; rewrite size_map size_enum_ord => i1ltn1. have iltn1 := ltnW i1ltn1. rewrite !(nth_map ord0) -?enumT ?size_enum_ord //=. rewrite -[i]/(val (Ordinal iltn1)) nth_ord_enum. rewrite -[succn i]/(val (Ordinal i1ltn1)) nth_ord_enum. set io := Ordinal iltn1; set io1 := Ordinal i1ltn1. rewrite /= !inE /= negb_and -!leqNgt. rewrite !permKV /= ltnSn leqnSn /= orbT !andbT. by rewrite -neq_ltn eq_sym orbN. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(fingroup perm morphism presentation) mathcomp(ssralg poly ssrint) permcomp tools permuted combclass congr