proposition: Lemma FA_gen m n: FA m.+1 (m.+1+n) = FA n m.+1 + FA n m.
proof: Proof. suff H: forall u v k1 k2, u + v < k1 -> u + v < k2 -> FA_rec u v k1 = FA_rec u v k2. have ha: n + m.+1 < m.+1 + (m.+1 + n). by rewrite addnC ltn_add2l addSn ltnS leq_addl. have hb: n + m.+1 < (n + m.+1).+1 by rewrite ltnSn. have hc: n + m < m.+1 + (m.+1 + n). by rewrite addSn ltnS addnA addnC leq_add2r leq_addr. have hd: n + m < (n + m).+1 by apply: ltnSn. rewrite /FA {1} /FA_rec addKn subn1 succnK ltnNge leq_addr. by rewrite - (H n m.+1 _ _ ha hb) - (H n m _ _ hc hd). move => u v; move: {2 3 4} (u+v) (leqnn (u+v)) => k. clear m n; elim: k u v. move => u v; rewrite leqn0 addn_eq0 => /andP [/eqP -> /eqP ->]. case => // k1; case => //. move => n Hrec u v luv; case => // k1; case => // k2; rewrite !ltnS => la lb. move: luv; case: u => // u; rewrite addSn ltnS /=. case(ltnP v u.+1) => // luv l2. have ha: v - u.+1 + u.+1 <= n by rewrite (subnK luv) (leq_trans _ l2)?leq_addl. have hb: v - u.+1 + (u.+1 - 1) <= n. by apply: leq_trans ha; rewrite leq_add2l leq_subr. by rewrite /= (Hrec _ _ ha k1 k2 la lb) (Hrec _ _ hb k1 k2). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)