proposition: Lemma f_correct: f_spec f.
proof: Proof. move => n; rewrite /f f_eqn /f1; apply: psum_exten => k kn. by rewrite /extension; case: (lt_dec k n) => //; rewrite kn. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)