proposition: Lemma GRr_b1 B: GRr B 1 = 1.
proof: Proof. rewrite /GRr; set E := [set t | _];set v := [set (@ord0 B) ]. suff: [set v] = E by move => <-; rewrite cards1. apply/ setP => x; rewrite !inE - Zeck_val_cv1; apply/eqP/eqP => h. by rewrite h /v /seto_to_seq enum_set1 /= Zeckv_cons Zeckv_nil. have eqa: (seto_to_seq x) = [::0]. move: h; case: (seto_to_seq x); first by rewrite Zeckv_nil. move => a l; rewrite Zeckv_cons; case: a. rewrite /fib/= addn0 - {2}(addn0 1) => /eqP; rewrite eqSS; case: l => //. by move => b l /eqP h; move:(Zeckv_pos b l); rewrite h. move => n. move:(leq0n n); rewrite - ltnS => /fib_smonotone_bis => h1 h2. by move: (leq_trans h1 (leq_addr (Zeck_val l) (fib n.+3))); rewrite h2. rewrite - (seto_to_seqK x) eqa /seq_to_seto /v /=. move: (inord_val (@ord0 B)) => /= eqb. apply/setP => i; rewrite inE eqb; apply/imsetP/eqP. by move=> [y ]; rewrite inE => /eqP ea ->. by move => ->; exists ord0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)