proposition: Lemma f_spec_simp f n: f_spec f -> f n = 2 ^ n.
proof: Proof. move => fs. elim: n; first by rewrite fs /f_spec /psum big_ord0. move => n Hrec. rewrite fs /f_spec /psum big_ord_recr /= addnC - addnS. by rewrite -/(psum f n) - fs Hrec addnn expnS mul2n. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)