proposition: Lemma GRr_big B n: n <= B -> GRr B n = GR n.
proof: Proof. rewrite /GR => lnb; symmetry; apply:GRr_big0 => //. by apply: leq_trans (fib_gen n.+2). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)