proposition: Lemma injective_w : injective w.
proof: Proof. move=> i j; case/boolP : (w i == 0); rewrite w_eq0 => i0. rewrite (eqP i0) wE0. case/boolP : (w j == 0); rewrite w_eq0 => j0; first by rewrite (eqP j0). by move/esym/eqP; rewrite w_eq0 (negbTE j0). case/boolP : (w j == 0) => [|]; rewrite w_eq0 => j0. by rewrite (eqP j0) wE0 => /eqP; rewrite w_eq0 (negbTE i0). case/boolP : (i == j) => [/eqP //|ij]. wlog : i j i0 j0 ij / i < j. move=> Hwlog H. move: ij; rewrite neq_ltn => /orP[|] ij. - apply Hwlog => //; by move/negbT : (ltn_eqF ij). - apply/esym; apply Hwlog => //; by move/negbT : (ltn_eqF ij). move=> {}ij /esym. rewrite /w (bigID (fun i1 : 'I__ => i1 < i)) /=. set a := (X in X + _ = _ -> _). set b := (X in _ = X -> _). set c := (X in _ + X = _ -> _). have ab : a >= b. rewrite {}/a {}/b big_ord_narrow; [exact: ltnW|move=> H]. apply: leq_sum => k _; rewrite leq_exp2l ?card_ord // leq_sub //. by apply/(sorted_ltn_nth leq_trans) => //; rewrite inE l_n. have c0 : 0 < c. rewrite {}/c lt0n sum_nat_eq0 negb_forall. apply/existsP; exists (Ordinal ij); by rewrite /= ltnn /= expn_eq0 card_ord. move=> acb; exfalso. move/eqP/negP : acb; apply; apply/negP/negbT/gtn_eqF; by rewrite -addn1 leq_add. Qed.
imports: mathcomp(all_ssreflect path ssralg ssrnum) ssr_ext