proposition: Lemma Z_to_little_endian_succ m n z : 0 ≤ m → Z_to_little_endian (Z.succ m) n z = Z.land z (Z.ones n) :: Z_to_little_endian m n (z ≫ n).
proof: Proof. unfold Z_to_little_endian. intros. by rewrite !iter_nat_of_Z, Zabs2Nat.inj_succ by lia. Qed.
imports: stdpp(options)