proposition: Lemma f_spec_simp1 f n: (forall n, ~~odd n -> f n = f_spec f n) -> f (n.*2.+2) = n.
proof: Proof. by move => h; rewrite f_spec_simp //= ?uphalf_double // odd_double. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)