Search code examples
coqtheorem-proving

How to prove (forall n m : nat, (n <? m) = false -> m <= n) in Coq?

How to prove forall n m : nat, (n <? m) = false -> 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 <-> n < m, but I don't know how to apply this since it only deals with (n <? m) = true, not (n <? m) = false.

Solution

  • Here is a proof that uses induction on n.

    Require Import NPeano.

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