https://github.com/coq-ext-lib/coq-ext-lib
Tip revision: 2b9b50da7d642e56d23cfd6c59911ea8559d5f24 authored by Pierre Roux on 31 January 2024, 11:18:40 UTC
Adapt to https://github.com/coq/coq/pull/18590
Adapt to https://github.com/coq/coq/pull/18590
Tip revision: 2b9b50d
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.