proposition: Lemma getBit_zero: forall n k, getBit (n := n) #0 k = false.
proof: Proof. move=> n k. rewrite fromNat0 /zero /copy /getBit nth_nseq if_same //. Qed.
imports: Coq(ZArith.ZArith) mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq fintype tuple div zmodp ssralg) ssrextra.nat ssrextra.tuple spec.spec