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