proposition: Lemma ZToOneC_OneCToZ: forall (sz : nat) (w : word sz), w <> wzero _ -> ZToOneC (OneCToZ w) = w.
proof: Proof. unfold ZToOneC. destruct sz; intros. - rewrite shatter_word_0; reflexivity. - rewrite normalizeZ_OneCToZ. unfold OneCToZ. destruct (wmsb _ _) eqn:Heqb; destruct (wordToN _) eqn:Heqn. + apply wordToN_wzero' in Heqn. apply wnot_inj. rewrite wnot_wones_wzero. auto. + apply wnot_inj; rewrite wnot_involutive. change (posToWord sz p) with (NToWord sz (N.pos p)). rewrite <- Heqn, waddmsb_NToWord, NToWord_wordToN. * reflexivity. * eapply wordToN_bound_wmsb_false. rewrite wmsb_wnot, Heqb; reflexivity. + apply wordToN_wzero' in Heqn. congruence. + change (posToWord sz p) with (NToWord sz (N.pos p)). rewrite <- Heqn. rewrite waddmsb_NToWord, NToWord_wordToN. * reflexivity. * eapply wordToN_bound_wmsb_false; eassumption. 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