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?
That's not true if a = 0.
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: Feb 08 2023 at 23:03 UTC