proposition: Lemma GARr_aux n B (g: ({set 'I_n.+1} -> {set 'I_B.+1}) := (fun t => [set (inord (i:'I_n.+1)) | i in t])): n <= B -> (injective g /\ forall (t:{set 'I_n.+1}) (F: nat -> nat), \sum_(i in t) F i= \sum_(i in (g t)) F i).
proof: Proof. rewrite -ltnS => lenB. set f: ('I_n.+1 -> 'I_B.+1) := fun i => inord i. pose Hw x := (inordK (leq_trans (ltn_ord x) lenB)). have Ha: injective f. move => i j; rewrite /f => sa. move:(f_equal (@nat_of_ord B.+1) sa); rewrite (Hw i) (Hw j); apply:ord_inj. split. rewrite /g => x y si; apply /setP => i; apply/idP/idP => ha. have: (f i) \in [set f i | i in x] by apply/imsetP; exists i. by rewrite si => /imsetP [t ty /Ha ->]. have: (f i) \in [set f i | i in y] by apply/imsetP; exists i. by rewrite - si => /imsetP [t ty /Ha ->]. move => t F. rewrite - (Zeck_val_cv0 t) - (Zeck_val_cv0 (g t)). apply: perm_big; apply: uniq_perm. + rewrite map_inj_uniq; [ apply: enum_uniq | apply: ord_inj]. + rewrite map_inj_uniq; [ apply: enum_uniq | apply: ord_inj]. + rewrite /seto_to_seq => i; rewrite /g;apply /mapP/idP. move => [x]; rewrite mem_enum => xt ->. by rewrite -(Hw x) map_f // mem_enum; apply /imsetP; exists x. move/mapP => [j];rewrite mem_enum; move/imsetP => [k kt -> ->]. by apply/mapP; rewrite (Hw k) map_f // mem_enum. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)