proposition: Lemma f_spec_simp f n: (forall n, f n = f_spec f n) -> f n = n.-1.
proof: Proof. move => H; case: n; first by rewrite H. elim; first by rewrite H. by move => n Hr; rewrite H /f_spec Hr Hr /=. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)