proposition: Lemma natToWord_wlt sz : forall n n' : nat, BinNat.N.lt (BinNat.N.of_nat n) (Npow2 sz) -> BinNat.N.lt (BinNat.N.of_nat n') (Npow2 sz) -> lt n n' -> wlt (natToWord sz n) (natToWord sz n').
proof: Proof. unfold wlt; intros. rewrite !wordToN_nat. rewrite !wordToNat_natToWord_idempotent; eauto. unfold BinNat.N.lt; rewrite <- Nnat.Nat2N.inj_compare. eapply Compare_dec.nat_compare_lt; eassumption. Qed.
imports: Bedrock.Word Fiat.Common.DecideableEnsembles