proposition: Lemma not_ltb2: forall (n0 n1 i: N), (n1 >= n0 + i)%N -> (n1 <? n0 + i)%N = false.
proof: Proof. intro n0. induction n0. intros. simpl in *. now apply N.ltb_nlt in H. intros. simpl. case_eq i. intros. subst. simpl in H. now apply N.ltb_nlt in H. intros. subst. apply N.ltb_nlt in H. now rewrite Npos_dist. Qed.
imports: Int63 PArray SMT_classes ZArith Misc State SMT_terms BVList Psatz Bool List BoolEq NZParity Nnat BinPos BinNat Pnat Init.Peano ProofIrrelevance