proposition: Lemma mul_int n m : \F n * \F m = \F (n *m)%N.
proof: Proof. case: n; first by rewrite T1mul0n. move => n;case: m; first by rewrite T1muln0 muln0. by move => m /=; rewrite - mulnE mulnSr addnC. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)