Various minor improvements

Author: hivert

theories/Combi/bintree.v

@@ -1456,8 +1456,7 @@ apply/idP/idP.
     suff -> : t1 = t2 by apply: le_refl.
     apply/val_inj/eqP => /=.
     have [Hsum2 Heq] := vctleq_sumn_right_sizes Hleq.
-    rewrite -Heq; apply/eqP/anti_leq.
-    by rewrite Hsum Hsum2.
+    by rewrite -Heq eqn_leq Hsum Hsum2.
   case: (t1 =P t2) => [-> | /eqP Hneq]; first by apply: le_refl.
   have [/= tt [Hrot Htleq]] := vctleq_rotation Hleq Hneq.
   have Hszt : size_tree tt == n by rewrite (size_rotations Hrot) bintreeszP.

theories/Combi/partition.v

@@ -760,9 +760,7 @@ Proof.
 move=> Hpart.
 case: c => //= c _.
 rewrite (conj_leqE Hpart) (conj_ltnE Hpart) /=.
-apply/idP/idP.
-- by move/eqP ->; rewrite !leqnn.
-- by move=> H; apply/eqP; exact: anti_leq.
+by apply/idP/idP => [/eqP ->|]; rewrite ?leqnn // -eqn_leq.
 Qed.
 
 Lemma rem_corner_incr_first_n sh i :

theories/Combi/skewpart.v

@@ -317,7 +317,7 @@ apply (iffP eqP); case: ex_minnP => m eqdrop mmin.
   + rewrite -eqmp1 => i lemi.
     by rewrite -(subnKC lemi) -!nth_drop (eqP eqdrop).
 - move=> [Hneq Heq].
-  apply anti_leq; apply/andP; split.
+  apply/anti_leq/andP; split.
   + apply: mmin; apply/eqP/(eq_from_nth_notin (x0 := x0)); first last.
       by move=> i; rewrite !nth_drop addSn; apply: Heq; rewrite ltnS leq_addr.
     * by apply/contra: x0notint => /mem_drop.
@@ -1571,7 +1571,7 @@ split => [i|i||i]; first 2 last; first exact: start_ltn.
   rewrite /mindropeq; case: ex_minnP => [[//|m]] /eqP Hdrop _ _ /= ltmi.
   by rewrite -(subnKC ltmi) -!nth_drop Hdrop.
 have conn4sym : connect_sym neig4 := @conn4_sym _ _.
-move=> Hi; apply anti_leq; apply/andP; split.
+move=> Hi; apply/anti_leq/andP; split.
   move/includedP: incl => [_ /(_ i)]; rewrite leq_eqVlt => /orP[/eqP-> | lti].
     by move/is_partP: partout => [_/(_ i)/leq_trans]; apply.
   have Hb : in_skew inner outer (i, nth 0 inner i) by rewrite /in_skew /= leqnn.

theories/Combi/std.v

@@ -310,7 +310,7 @@ set pos := (posbig s).+1; set LR := take _ _.
 have HposLR : pos = size LR.
   rewrite /LR size_take /pos size_std_rec.
   case: (ltnP (posbig s).+1 (size s)) => Hpos; first by [].
-  apply/eqP; rewrite eqn_leq Hpos andbT.
+  apply: anti_leq; rewrite Hpos andbT.
   have: s != [::] by move: Hmax; case s.
   exact: posbig_size.
 rewrite HposLR; apply/eqP; rewrite -posbigE.
@@ -948,7 +948,7 @@ Qed.
 Lemma size_invseq s t : invseq s t -> size s = size t.
 Proof.
 rewrite /invseq => /andP[Hst Hts].
-by apply/eqP; rewrite eqn_leq !size_leq_invseq.
+by apply: anti_leq; rewrite !size_leq_invseq.
 Qed.
 
 Lemma linvseq_subset_iota s t : linvseq s t -> {subset iota 0 (size s) <= t}.

theories/LRrule/Greene.v

@@ -513,7 +513,7 @@ Qed.
 Lemma Greene_rel_t_0 : Greene_rel_t 0 = 0.
 Proof using.
 rewrite /Greene_rel_t /=.
-apply/eqP; rewrite eqn_leq; apply/andP; split; last by [].
+apply/anti_leq/andP; split; last by [].
 apply/bigmax_leqP => S.
 rewrite /ksupp => /and3P[HS _ _].
 have -> : S = set0 by apply/eqP; rewrite -cards_eq0 eqn_leq HS.
@@ -734,7 +734,7 @@ Hypothesis HnegR : transitive negR.
 Lemma Greene_rel_seq r k : sorted negR r -> Greene_rel r k = minn (size r) k.
 Proof using HnegR.
 move=> Hrow /=.
-apply/eqP; rewrite eqn_leq; apply/andP; split; last exact: Greene_rel_t_inf.
+apply/anti_leq/andP; split; last exact: Greene_rel_t_inf.
 rewrite leq_min Greene_rel_t_sup /=; apply/bigmax_leqP => s.
 rewrite /ksupp /trivIset => /and3P[Hcard /eqP /= <- /forallP Hsort].
 suff {Hcard} H B : B \in s -> #|B| <= 1.
@@ -883,7 +883,7 @@ Qed.
 Lemma Greene_rel_rev (leT : rel Alph) u :
   Greene_rel leT u =1 Greene_rel (fun y x => leT x y) (rev u).
 Proof using.
-move=> k; apply anti_leq; apply/andP; split.
+move=> k; apply/anti_leq/andP; split.
 - apply leq_Greene; first exact: ksupp_inj_rev.
 - rewrite [X in _ <= X](eq_Greene_rel (R2 := fun x y => leT x y)).
   + apply leq_Greene; rewrite -{2}(revK u); exact: ksupp_inj_rev.
@@ -1600,7 +1600,7 @@ Qed.
 Theorem Greene_row_tab k t :
   is_tableau t -> Greene_row (to_word t) k = sumn (take k (shape t)).
 Proof using.
-move=> Htab; apply/eqP; rewrite eqn_leq; apply/andP; split.
+move=> Htab; apply/anti_leq/andP; split.
 - rewrite -(conj_partK (is_part_sht Htab)) -sum_conj.
   rewrite (shape_tabcols Htab) /Greene_row /Greene_rel /Greene_rel_t.
   apply/bigmax_leqP => /= U; rewrite /ksupp => /and3P[Hsz Htriv].
@@ -1623,7 +1623,7 @@ Theorem Greene_col_tab k t :
   is_tableau t -> Greene_col (to_word t) k = sumn (take k (conj_part (shape t))).
 Proof using.
 move=> Htab; rewrite -sum_conj.
-apply/eqP; rewrite eqn_leq /=; apply/andP; split.
+apply/anti_leq/andP; split.
 - elim: t Htab => [_ | t0 t IHt] /=.
     by apply: (@leq_trans 0); first exact: Greene_rel_t_sup.
   move=> /and4P[_ Hrow _ /IHt{IHt} Ht]; rewrite to_word_cons.