https://github.com/coq-ext-lib/coq-ext-lib
Tip revision: 26626fa42c0c8a488522781bf867607531c4528e authored by Pierre Rousselin on 21 October 2023, 16:47:49 UTC
Adapt to Coq/Coq#18164
Adapt to Coq/Coq#18164
Tip revision: 26626fa
ConsiderDemo.v
Require Import Coq.Bool.Bool.
Require Import Arith.PeanoNat.
Require Import ExtLib.Tactics.Consider.
Require Import ExtLib.Data.Nat.
Require Import Coq.ZArith.ZArith.
Require Import Coq.micromega.Lia.
Set Implicit Arguments.
Set Strict Implicit.
(** Some tests *)
Section test.
Goal forall x y z, (Nat.ltb x y && Nat.ltb y z) = true ->
Nat.ltb x z = true.
intros x y z.
consider (Nat.ltb x y && Nat.ltb y z).
consider (Nat.ltb x z); auto. intros. exfalso. lia.
Qed.
Goal forall x y z,
Nat.ltb x y = true ->
Nat.ltb y z = true ->
Nat.ltb x z = true.
Proof.
intros. consider (Nat.ltb x y); consider (Nat.ltb y z); consider (Nat.ltb x z); intros; auto.
exfalso; lia.
Qed.
End test.