proposition: Lemma Z_to_little_endian_bound m n z : 0 ≤ n → 0 ≤ m → Forall (λ b, 0 ≤ b < 2 ^ n) (Z_to_little_endian m n z).
proof: Proof. intros. revert z. induction m as [|m ? IH|] using (Z.succ_pred_induction 0); intros z; [..|lia]. { by constructor. } rewrite Z_to_little_endian_succ by lia. constructor; [|by apply IH]. rewrite Z.land_ones by lia. apply Z.mod_pos_bound, Z.pow_pos_nonneg; lia. Qed.
imports: stdpp(options)