proposition: Lemma GARr_e B n: GAr B (Zeckp n) n = GRr B n.
proof: Proof. rewrite /GAr/GRr; apply: eq_card => e; apply /idP/idP;rewrite !inE. by move/andP => []. move => /eqP <-; rewrite eqxx andbT - Zeck_val_cv1 - Zeck_valp_cv1. apply/eqP; symmetry; apply: Zeckp_prop1; apply:uniq_seto_to_seq. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)