proposition: Lemma GAr_notz B m n: GAr B m n!= 0 -> m = Zeckp n.
proof: Proof. rewrite /GAr cards_eq0 => /set0Pn [x ];rewrite inE => /andP [/eqP pa /eqP pb]. move:(Zeck_val_cv1 x) (Zeck_valp_cv1 x); rewrite - pa - pb => <- <-. 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)