Stream: Coq users

Topic: diffenent form

sara lee (Aug 02 2022 at 18:00):

Theorem a_value : forall (a:nat),
 a - 1 + 1 = a.

To solve above ,which lemma (related to minus sign between two terms ) i should apply here?

Lessness (Aug 02 2022 at 18:18):

That's not true if a = 0.

Pierre Jouvelot (Aug 02 2022 at 18:18):

Note that this theorem is wrong if a = 0, since 0 - 1 = 0. If you use mathcomp, you can find a lemma to prove the following variant:

From mathcomp Require Import all_ssreflect.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Theorem a_value : forall (a:nat),
    0 < a -> a - 1 + 1 = a.
Proof.
move=> a lt0a.
Search (_ - ?n + ?n).
by rewrite subnK.
Qed.

Last updated: Oct 13 2024 at 01:02 UTC