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