proposition: Lemma not_ltb: forall (n0 n1 i: N), (n1 <? n0 + i)%N = false -> n1 >= n0 + i.
proof: Proof. intro n0. induction n0. intros. simpl in *. apply N.ltb_nlt in H. apply N.nlt_ge in H. lia. intros. simpl. case_eq i. intros. subst. simpl in H. apply N.ltb_nlt in H. apply N.nlt_ge in H. intros. simpl in H. lia. intros. subst. apply N.ltb_nlt in H. apply N.nlt_ge in H. lia. Qed.
imports: List Bool NArith Psatz Int63 Nnat ZArith Misc ProofIrrelevance