proposition: Lemma rev7_lb n (Hn : 2 < n) : 2 ^ n.-1 <= 7 * 2 ^ (n - 3).
proof: Proof. destruct n => //=. rewrite (@leq_trans (2 ^ 2 * 2 ^( n.+1 - 3))) //. rewrite -expnD leq_exp2l // addnBA // addnC addn2 -addn3. by rewrite -addnBA // subnn addn0. by rewrite leq_pmul2r // expn_gt0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype tuple) BinPos BinNat PArith ssr_ext