make fset_set_sub an equality

theories/cardinality.v

@@ -712,10 +712,11 @@ by move=> fA x; rewrite -[A in RHS]fset_setK//; apply/idP/idP; rewrite ?inE.
 Qed.
 
 Lemma fset_set_sub (T : choiceType) (A B : set T) :
-  finite_set A -> finite_set B -> A `<=` B -> (fset_set A `<=` fset_set B)%fset.
+  finite_set A -> finite_set B -> A `<=` B = (fset_set A `<=` fset_set B)%fset.
 Proof.
-move=> finA finB AB; apply/fsubsetP => t.
-by rewrite in_fset_set// in_fset_set// 2!inE => /AB.
+move=> finA finB; apply/propext; split=> [AB|/fsubsetP AB t].
+  by apply/fsubsetP => t; rewrite in_fset_set// in_fset_set// 2!inE => /AB.
+by have := AB t; rewrite !in_fset_set// !inE.
 Qed.
 
 Lemma fset_set_set0 (T : choiceType) (A : set T) : finite_set A ->

theories/measure.v

@@ -1673,10 +1673,10 @@ move=> /(_ K (leqnn _)); rewrite leNgt => /negP; apply.
 rewrite sumFE lte_fin ltr_nat ltnS.
 have -> : k = #|` fset_set (\bigcup_n F n) |.
   by apply/esym/card_eq_fsetP; rewrite fset_setK//; exists k.
-apply/fsubset_leq_card/fset_set_sub => //.
+apply/fsubset_leq_card; rewrite -fset_set_sub //.
+- by move=> /= t; rewrite -bigcup_mkord => -[m _ Fmt]; exists m.
 - by rewrite -bigcup_mkord; exact: bigcup_finite.
 - by exists k.
-- by move=> /= t; rewrite -bigcup_mkord => -[m _ Fmt]; exists m.
 Unshelve. all: by end_near. Qed.
 
 HB.instance Definition _ := isMeasure.Build _ _ counting

theories/sequences.v

@@ -1238,7 +1238,7 @@ Qed.
 
 Definition nseries (u : nat^nat) := (fun n => \sum_(0 <= k < n) u k)%N.
 
-Lemma le_nseries (u : nat^nat) : {homo nseries u : a b / (a <= b)%N}.
+Lemma le_nseries (u : nat^nat) : {homo nseries u : a b / a <= b}%N.
 Proof.
 move=> a b ab; rewrite /nseries [in X in (_ <= X)%N]/index_iota subn0.
 rewrite -[in X in (_ <= X)%N](subnKC ab) iotaD big_cat/= add0n.