proposition: Lemma GRr_notz B n: fib B.+4 <= n.+1 -> GRr B n = 0.
proof: Proof. suff: GRr B n != 0 -> n.+2 <= fib B.+4. by move/contraR; rewrite -leqNgt => h h1; apply/eqP/h. rewrite cards_eq0 => /set0Pn [x ];rewrite inE => /eqP pa. rewrite -pa -(Zeck_val_cv1 x). apply: (Zeckv_bound3 (uniq_seto_to_seq x)). by apply/allP => i /mapP [j _ ->];case:j. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)