proposition: Theorem leperm_invset s t : (s <=R t) = (invset s \subset invset t).
proof: Proof. apply/idP/idP => [/lepermP/= [u]->{t} | H]. rewrite -{-2}(canwordP u) -(size_canword u). elim/last_ind: (canword u) (canword_reduced u) => [| w i IHw]. by rewrite big_nil /= mulg1 => _. rewrite size_rcons -cats1 big_cat /= big_cons big_nil mulg1. move/reduced_catl => Hred; rewrite -(reducedP Hred). move/(_ Hred): IHw; move: Hred => /reducedP <-. move: (\prod_(i <- w) _) => /= P IHP. rewrite mulgA -(addn1 (length P)) addnA -(length_eltr i) => Hlen. move/(_ (lengthKL Hlen)): IHP => /subset_trans; apply. pose il := lift ord_max i. have Hi : il < n0 by rewrite /il lift_max ltn_ord. have Hsi : 's_i = 's_il :> 'S_n by rewrite lift_max. rewrite Hsi invset_eltrR //; first exact: subsetU1. by rewrite length_descR // -{}Hsi Hlen (lengthKL Hlen) length_eltr addn1 ltnS. have /subnKC: length s <= length t by rewrite /length subset_leq_card. move: (length t - length s) => d Hd. move: H; elim: d => [|d IHd] in t Hd *. move=> H; move: Hd; rewrite addn0 /length => /eqP. rewrite (subset_leqif_cards H) => /eqP/invset_inj ->. exact: le_refl. rewrite subEproper=> /orP[/eqP/invset_inj-> | ]; first exact: le_refl. move/properP => /= [incl ex]. have {ex} /ex_minnP[m /existsP[[/= i j]] /=] : exists n : nat, [exists p, [&& p \in invset t, p \notin invset s & t p.1 - t p.2 == n]]. move: ex => [[i j]] ijt ijNs; exists (t i - t j). by apply/existsP => /=; exists (i, j) => /=; apply/and3P. rewrite [in X in (X-> _ -> _)]/invset !inE /= => /and3P[/andP[iltj tjltti]]. rewrite iltj /= -leqNgt leq_eqVlt (inj_eq val_inj) (inj_eq perm_inj). rewrite -[i == j](inj_eq val_inj) (ltn_eqF iltj) /= => siltsj /eqP eqm Hm. have m0 : 0 < m by case: m eqm {Hm} => // /eqP; rewrite subn_eq0 leqNgt tjltti. have Hti : t i = t j + m :> nat. rewrite -eqm {Hm} in m0; rewrite -eqm subnKC //. by apply ltnW; rewrite -subn_gt0. have {}Hm (k l : 'I_n) : (k, l) \in invset t -> (k, l) \notin invset s -> m <= t k - t l. move=> pIt pNIs; apply Hm; apply/existsP; exists (k, l). by rewrite pIt pNIs eq_refl. have {Hm m0 eqm tjltti} Heq : m = 1%N. have {}incl (k l : 'I_n) : k < l -> s k > s l -> t k > t l. by move=> kltl; move: incl => /subsetP/(_ (k, l))/[!inE]/[!kltl]. apply anti_leq; rewrite {}m0 andbT {Hd IHd}. rewrite leqNgt; apply/negP => Habs. pose k := (t^-1 (inord (t j).+1)). have tk : t k = (t j).+1 :> nat. by rewrite /k permKV inordK // ltnS (leq_trans tjltti _) // -ltnS. suffices []: (m <= t k - t j) \/ (m <= t i - t k). - by rewrite tk subSn // subnn => /(leq_trans Habs)/[!ltnn]. - rewrite tk -eqm. case: (val (t i)) tjltti => //= u /[!ltnS] Hu. by rewrite subSS subSn // ltnn. case: (ltngtP k i) => [klti | iltk | /val_inj Hk]; last 1 first. - by move: Habs; rewrite -eqm -Hk tk subSn // ?subnn ltnn. - left; have kltj := ltn_trans klti iltj. apply: Hm; rewrite inE /= kltj /= ?tk //. rewrite -leqNgt; apply ltnW; apply: (leq_trans _ siltsj). rewrite leqNgt ltnS; apply/negP => siltsk. have:= incl k i klti siltsk. by rewrite tk ltnS leqNgt tjltti. have {tjltti} tkltti : t k < t i. rewrite tk {}Hti {eqm Hm}; case: m Habs => [|[|m]]// _. by rewrite !addnS !ltnS leq_addr. case: (ltngtP k j) => [kltj | jltk | /val_inj Hkj]; last first. - exfalso; move: Hkj => /(congr1 t)/(congr1 val)/=/eqP. by rewrite tk eqn_leq ltnn. - right; apply: Hm; rewrite inE /= iltk //=. move: incl => /(_ j k jltk)/contra; rewrite -!leqNgt => incl. have {}/incl : t j <= t k by rewrite tk. exact: leq_trans (ltnW siltsj). case: (ltnP (s i) (s k)) => [siltsk | sklesi]. - right; apply: Hm; rewrite inE /= iltk //=. by rewrite -leqNgt; exact: ltnW. case: (ltnP (s k) (s j)) => [skltsj | sjlesk]. - left; apply: Hm; rewrite inE /= kltj /= ?tk //. by rewrite -leqNgt; apply ltnW. - by have:= leq_trans siltsj (leq_trans sjlesk sklesi); rewrite ltnn. rewrite {}Heq addn1 in Hti. have tjn0 : t j < n0 by rewrite -ltnS -Hti. have {Hti} Himj : (t * 's_(t j))^-1 (t j) = i. by rewrite invMg !permM eltrV eltrL -Hti inord_val !permK. have Himi : (t * 's_(t j))^-1 (inord (succn (t j))) = j. by rewrite invMg !permM eltrV eltrR !permK. have Hdesc : (t * 's_(t j))^-1 (t j) < (t * 's_(t j))^-1 (inord (succn (t j))). by rewrite Himi Himj. have Hln : (length (t * 's_(t j))).+1 = length t. by rewrite -[in RHS](mulgK 's_(t j) t) eltrV [RHS]length_add1R. have {Hd Hln} {}/IHd IHd : length s + d = length (t * 's_(t j)). by move: Hd; rewrite -Hln addnS => [] []. have {Himi Himj} invsett : invset t = (i, j) |: invset (t * 's_(t j)). by rewrite -{1}Himi -Himj -(invset_eltrR tjn0 Hdesc) -{2}eltrV mulgK. have {invsett} {}/IHd : invset s \subset invset (t * 's_(t j)). move: incl; rewrite {}invsett => /subsetP Hsubs. apply/subsetP => /= [[k l] H]. move/(_ _ H): Hsubs => /[!inE] /orP[] // /eqP Heq. exfalso; move: H; rewrite {}Heq /invset !inE /= iltj /=. by rewrite ltnNge (ltnW siltsj). move/le_trans; apply. rewrite -{3}(mulgK 's_(t j) t) eltrV. apply/lepermP; exists 's_(t j) => //. by rewrite (length_eltr (Ordinal tjn0)) addn1; exact: length_add1R. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(fingroup perm morphism presentation) permcomp tools permuted combclass congr presentSn ordtype