proposition: Lemma _of_bits_size l s: (size (_of_bits l s)) = s.
proof: Proof. unfold of_bits, size. unfold _of_bits. case_eq ( N.of_nat (length l) =? s)%N. intros. now rewrite N.eqb_eq in H. intros. unfold zeros. rewrite length_mk_list_false. now rewrite N2Nat.id. Qed.
imports: List Bool NArith Psatz Int63 Nnat ZArith Misc ProofIrrelevance