proposition: Lemma wle_antisym x : forall y, wlt x y = false -> wlt y x = false -> x = y.
proof: Proof. intros. rewrite wlt_false_iff in *. unfold Word.wlt in *. rewrite BinNat.N.nlt_ge in *. apply Word.wordToN_inj. apply BinNat.N.le_antisymm; intuition. Qed.
imports: Fiat.FiniteSetADTs.WordInterface Bedrock.Memory Bedrock.IL