proposition: Lemma f_spec_simp2 f n: (forall n, f n = f_spec f n) -> f(n.*2.+3) = n.
proof: Proof. move => h. have hh: forall n, f (n.*2.+2) = n. move => m; apply: f_spec_simp1 => k _; apply: h. by elim: n; [ by rewrite h | move => n Hr; rewrite h /= Hr hh]. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)