proposition: Lemma FA_prop0bis a b: (Zeckp b).+1 = a -> FA a b = 0.
proof: Proof. move => eq1; case eq2:(FA a b == 0); first by rewrite (eqP eq2). by move: (n_Sn (Zeckp b)); rewrite eq1 (FA_nz (negbT eq2)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)