proposition: Lemma f_correct n: ~~odd n -> f n = f_spec f n.
proof: Proof. case: n;first by rewrite /f /= f_eqn. case => //; case; first by rewrite /f /= f_eqn. case => // n; rewrite /f_spec /f f_eqn /f1 /=. case: (odd_dec n) => a b. by move: (negbNE (negbNE b)); move /negP; case. by case:(f2 n.+2) => x p /=;case: (f0a a p) => y q; case:(f2 x.*2.+2). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)