proposition: Lemma sub_int n m : \F n - \F m = \F (n -m)%N.
proof: Proof. case: n m => // n [] // m /=. rewrite subSS /T1nat; case (ltngtP n m) => pa. - by rewrite (eqP (ltnW pa)). - by rewrite -(subnSK pa). - by rewrite pa subnn. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)