proposition: Lemma rev7_ub n (Hlen : 2 < n) : 7 * 2 ^ (n - 3) < 2 ^ n.
proof: Proof. rewrite -[in X in _ < X](@subnKC 3 n) //. by rewrite /= expnD ltn_pmul2r // expn_gt0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype tuple) BinPos BinNat PArith ssr_ext