Lemma binaryExpOctetsPad : forall x, List.length (binaryExpOctets (Pad x)) = N.to_nat x.
