proposition: Lemma wordToNat_lt sz : forall w w' : word sz, wlt w w' -> lt (wordToNat w) (wordToNat w').
proof: Proof. intros. unfold wlt, BinNat.N.lt in H. rewrite !wordToN_nat, <- Nnat.Nat2N.inj_compare, <- Compare_dec.nat_compare_lt in H. eassumption. Qed.
imports: Bedrock.Word Fiat.Common.DecideableEnsembles