proposition: Lemma add_int n m : \F n + \F m = \F (n +m)%N.
proof: Proof. by case: n m => // n [ | m]; rewrite /= - ? addnS // - addnE addn0. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)