proposition: Lemma wle_asym x : forall y, wlt x y = true -> wlt y x = false.
proof: Proof. intro y; rewrite wlt_true_iff, wlt_false_iff. unfold Word.wlt. apply BinNat.N.lt_asymm. Qed.
imports: Fiat.FiniteSetADTs.WordInterface Bedrock.Memory Bedrock.IL