Как доказать (forall n m: nat, (n <? M) = false -> m <= n) в Coq?

Question

Как доказать forall n m : nat, (n <? m) = false -> m <= n в Coq?

Я дошел до заключения до ~ n < m, используя apply Nat.nlt_ge.

Ведение SearchAbout ltb дает ltb_lt: forall n m : nat, (n <? m) = true <-> n < m, но я не знаю, как применить это, так как она имеет дело только с (n <? m) = true, не (n <? m) = false.

Answer 1

Вот доказательство, которое использует индукцию по 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.