proposition: Lemma BinNat_lt_of_nat_S: forall (p : nat) (q : BinNums.N), BinNat.N.lt (BinNat.N.of_nat (S p)) q -> BinNat.N.lt (BinNat.N.of_nat p) q.
proof: Proof. intros; Nomega.nomega. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Bedrock.Memory