Title: How to prove (forall n m : nat, (n <? m) = false -> m <= n) in Coq?
Tags: coq;theorem-proving
Question: How to prove ```forall n m : nat, (n <? m) = false -&gt; m <= n``` in Coq?

I got as far as turning the conclusion into ```~ n < m``` using by ```apply Nat.nlt_ge```.

Doing ```SearchAbout ltb``` yields ```ltb_lt: forall n m : nat, (n <? m) = true <-&gt; n < m```, but I don't know how to apply this since it only deals with ```(n <? m) = true```, not ```(n <? m) = false```.

Comment: Ah, I think I got it: `intros. apply Nat.ntl_ge. contradict H. apply Nat.ltb_lt in H. rewrite H. discriminate. Qed.`

Comment: Sorry typo, that should have been `Nat.nlt_ge`.

Comment: Where is `Nat.ntl_ge` defined?

Here is the accepted answer: Here is a proof that uses induction on n.

```Require Import NPeano.

Theorem my_thm: forall n m, (n <? m) = false -&gt; m <= n.
  induction n; destruct m; intros ; auto using (Le.le_n_S); discriminate.
Qed.
```



{'source': 'StackExchangeDataset', 'subset': 'stackoverflow.com', 'metadata': {'AnswerCount': 1, 'CommentCount': 3, 'ContentLicense': 'CC BY-SA 3.0', 'CreationDate': '2015:00:01/25/15', 'FavoriteCount': None, 'PostTypeId': 1, 'Tags': '<coq><theorem-proving>', 'Title': 'How to prove (forall n m : nat, (n <? m) = false -> m <= n) in Coq?', 'ViewCount': 673, 'id': 28141606, 'user_AboutMe': None, 'user_AccountId': 5682143.0, 'user_DisplayName': 'Atsby', 'user_Reputation': 2227.0, 'user_Views': 121.0, 'user_id': 4492918.0}}