proposition: Lemma Z_to_little_endian_length m n z : 0 ≤ m → Z.of_nat (length (Z_to_little_endian m n z)) = m.
proof: Proof. intros. revert z. induction m as [|m ? IH|] using (Z.succ_pred_induction 0); intros z; [done| |lia]. rewrite Z_to_little_endian_succ by lia. simpl. by rewrite Nat2Z.inj_succ, IH. Qed.
imports: stdpp(options)