H2: a=0 (while a is natural number). I am unable to solve it by lia. What could be the reason?
what's the error message?
This works :
Require Import Lia. Goal forall a, a>0 -> a=0 -> False. intros H1 H2. now lia. Qed.
Directly apply lia. Not written in this way Goal forall a, a>0 -> a=0 -> False. Whats the difference between these ways?
This was an answer to a part of of your previous post you moved later to another topic.
You may use the
Require Import List Arith Lia. Import ListNotations. Goal forall (A:Type) (x: A), In x  -> False. Proof. intros A x H. inversion H. Qed. Goal forall (A:Type) (x y:A) l, In x (y::l) -> x = y \/ In x l. Proof. intros A x y l H. inversion H. - left; congruence. - now right. Qed.
Last updated: Oct 04 2023 at 19:01 UTC