proposition: Lemma FAx_small m n: n < m -> GA m n = 0.
proof: Proof. move => h. case w: (GAr n m n == 0); first by rewrite /GA (eqP w). move: (GAr_notz (negbT w)) => ha. by move: h; rewrite (Zeckp_prop2 n) - ha ltnNge leq_addr. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)