proposition: Lemma lt_ptr_mod: forall n1 n2, n1 <= n2 <= Ptrofs.max_unsigned -> n1 <= n2 < Ptrofs.modulus.
proof: Proof. intros. replace Ptrofs.max_unsigned with (Z.pred Ptrofs.modulus) in * by (unfold Ptrofs.max_unsigned; lia). now rewrite <- Z.lt_le_pred in *. Qed.
imports: compcert.common.Events compcert.common.Memory compcert.common.Values compcert.common.AST compcert.lib.Integers Coq.ZArith.BinInt Coq.Lists.List Coq.micromega.Lia