proposition: Lemma GRr_big0 A B n: n < fib A.+3 -> A <= B -> GRr A n = GRr B n.
proof: Proof. rewrite /GRr => ns lenm. move:(GARr_aux lenm); set g := (fun t:_ => _); move => [Hb Hx]. move:lenm; rewrite - ltnS => lenm. pose Hw x := (inordK (leq_trans (ltn_ord x) lenm)). have Hc: forall t, Zeck_sval t = Zeck_sval (g t). move => t; apply: (Hx t (fun z => (fib z.+2))). set pn := [pred t : {set 'I_A.+1} | Zeck_sval t == n]. rewrite cardsE -(card_imset pn Hb). apply: eq_card => e; rewrite inE; apply/imsetP/idP. by move => [x]; rewrite inE Hc => ww ->. set l :=(seq_to_seto A (seto_to_seq e)) => eq. suff ww : e = g l by exists l => //; rewrite /pn inE Hc - ww. have Hd: forall i, i \in e -> i <= A. move => i ie. rewrite - 3!ltnS; apply:fib_monotone_bis; apply: leq_trans ns. rewrite ltnS -(eqP eq) - Zeck_val_cv1. by apply:Zeckv_bnd0; rewrite /seto_to_seq map_f // mem_enum. rewrite /l /g /seq_to_seto/seto_to_seq - map_comp /comp. apply/setP =>i; apply/idP/imsetP. move => ie; move:(inordK (Hd _ ie)) => sa. rewrite - mem_enum in ie; exists (inord i); last by rewrite sa inord_val. by apply /imsetP; exists (inord i) => //;rewrite (map_f _ ie). move => [j /imsetP [k /mapP [x]]];rewrite mem_enum => H. by move => -> -> -> /=; rewrite inordK ? inord_val // ltnS Hd. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)