时间戳

首页 > 解决方案 > 检查自然数的后继

coq - 检查自然数的后继

问题描述

我想证明一个目标，我有两个假设。你能帮我证明目标吗？非常感谢您的帮助。 Goal : (S m <? S m - (S m - 1)) = true有两个假设

m : nat
H : 1 < 1
H0 : (S  m =? 0) = false

标签： coq

解决方案

事实上，1 并不小于 1。因此，我们可以证明是荒谬的。好事，同样，因为目标本身是不可能的。

Require Import PeanoNat.
contradict H. (* now proving ~(1 < 1) *)
(* Well, < is irreflexive: forall x, ~(x < x). *)
apply Nat.le_irrefl.

推荐阅读