proposition: Lemma f0a y n: odd n = false -> odd n.+2 \/ y <= (n.+2)./2.-1 -> y <= n./2 /\ lte (y.*2).+2 n.+4.
proof: Proof. rewrite /lte /=; move =>h; rewrite h /= odd_double; case => // eq. split => //=. move: eq. rewrite - ltnS - ltn_double ltnS ltnS. rewrite - {2} (odd_double_half n) h add0n //. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)