proposition: Lemma rev7_neq0 n : (7 * 2 ^ (n - 3))%nat <> O.
proof: Proof. rewrite -[in X in _ <> X ](muln0 7). move/eqP. by rewrite eqn_mul2l /= expn_eq0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype tuple) BinPos BinNat PArith ssr_ext