proposition: Lemma f_correct n: f n = f_spec f n.
proof: Proof. case: n => //; case => // n. rewrite /f_spec /f f_eqn /f1. by case: (f2 n.+1) => y1 H1; case: (f2 y1.+1) => y2 H2. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)