proposition: Lemma f_spec_simp f n: ~~ odd n -> (forall n, ~~odd n -> f n = f_spec f n) -> f n = (n.-1)./2.
proof: Proof. move => on h1. have h2: forall n, f (n.*2) = f_spec f (n.*2). by move => h; apply: h1; rewrite odd_double. move: (odd_double_half n); rewrite (negbTE on) add0n => <-. set m := (n./2). move: m; case; first by rewrite h2. elim; first by rewrite h2 /=. move => k hk. rewrite h2 /f_spec doubleS doubleS - (doubleS k) hk. by rewrite doubleS /= uphalf_double - (doubleS k) hk doubleS /= uphalf_double. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)