proposition: Lemma normalizeZ_OneCToZ {sz} : forall w: word (S sz), normalizeZ sz (OneCToZ w) = (OneCToZ w).
proof: Proof. intros. apply normalizeZ_noop. unfold OneCToZ. pose proof (Npow2_ge_one sz). destruct (wmsb _ _) eqn:Heqb; destruct (wordToN _) eqn:Heqn; repeat match goal with | _ => lia | [ H: wordToN (wnot ?w) = _, Heqb: wmsb ?w _ = _ |- _ ] => apply (f_equal negb) in Heqb; rewrite <- (wmsb_wnot' (S sz) w true) in Heqb; simpl in Heqb | [ H: wmsb ?w ?b = _ |- _ ] => let w' := fresh in let Heqw := fresh in destruct (wmsb_combine w b) as (w' & Heqw); rewrite Heqw in Heqn; rewrite <- (Nat.add_1_r sz) in *; simpl in Heqn; clear Heqw; rewrite wordToN_combine in Heqn; pose proof (wordToN_bound w'); simpl in Heqn; rewrite Heqb in Heqn; simpl in Heqn end. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat List Bedrock.Word Coq.ZArith.ZArith Coq.micromega.Psatz NArith NArithRing ZArith ZArithRing Program Coq.micromega.Psatz AlignedByteString Permutation