proposition: Lemma FA_nz m n: FA m n != 0 -> m = Zeckp n.
proof: Proof. move: (leq_maxl m n) (leq_maxr m n); set s := (maxn m n). move:s => s; elim: s m n. by move => m n; rewrite !leqn0 => /eqP -> /eqP ->; rewrite Zeckp_0. move => b Hr m n; case: (ltngtP m n); last first. + move => -> _ _; rewrite FA_mm'; case n; first by rewrite Zeckp_0. by move => k; rewrite ltnS leqn0; case: k => //; rewrite Zeckp_1. + by move/FA_small => ->. + move => lemn _; rewrite leq_eqVlt; case/orP=> [|]; last first. by rewrite ltnS => nn; apply: (Hr _ _ (leq_trans (ltnW lemn) nn) nn). move: lemn; case:m; first by move => _ /eqP ->; rewrite FA_0S. move => m lmn /eqP nv. have lta: m.+1 <= b by rewrite - ltnS -nv. have ltc: (n - m.+1) <= b by rewrite -ltnS (subnSK (ltnW lmn)) -nv leq_subr. rewrite - (subnKC (ltnW lmn)) FA_gen addn_eq0 negb_and => /orP; case. by move /(Hr _ _ ltc lta) => ->; rewrite(Zeckp_prop3a m.+1). by move /(Hr _ _ ltc (ltnW lta)) => ->; rewrite (Zeckp_prop4a m.+1). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)