proposition: Lemma GRr_b0 B: GRr B 0 = 1.
proof: Proof. rewrite /GRr; set E := [set t | _];set v := (@set0 'I_B.+1). suff: [set v] = E by move => <-; rewrite cards1. apply/ setP => x; rewrite !inE - Zeck_val_cv1; apply/eqP/eqP => h. by rewrite h /seto_to_seq enum_set0 /= Zeckv_nil. case ee: (x==v); [by apply/eqP |move:(negbT ee) ]. move/set0Pn => [u]; rewrite - mem_enum - (mem_map (@ord_inj B.+1)). move: h; rewrite -/(seto_to_seq _ ); case (seto_to_seq x) => // a l bad. by move: (Zeckv_pos a l); rewrite bad. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)