proposition: Lemma little_endian_to_Z_to_little_endian m n z : 0 ≤ n → 0 ≤ m → little_endian_to_Z n (Z_to_little_endian m n z) = z `mod` 2 ^ (m * n).
proof: Proof. intros ? Hm. rewrite <-Z.land_ones by lia. revert z. induction m as [|m ? IH|] using (Z.succ_pred_induction 0); intros z; [..|lia]. { Z.bitwise. by rewrite andb_false_r. } rewrite Z_to_little_endian_succ by lia; simpl. rewrite IH by lia. apply Z.bits_inj_iff'. intros z' ?. rewrite Z.land_spec, Z.lor_spec, Z.shiftl_spec, !Z.land_spec by lia. rewrite (Z.ones_spec n z') by lia. case_bool_decide. - rewrite andb_true_r, (Z.testbit_neg_r _ (z' - n)), orb_false_r by lia. simpl. by rewrite Z.ones_spec, bool_decide_true, andb_true_r by lia. - rewrite andb_false_r, orb_false_l. rewrite Z.shiftr_spec by lia. f_equal; [f_equal; lia|]. rewrite !Z.ones_spec by lia. apply bool_decide_ext. lia. Qed.
imports: stdpp(options)