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