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