Library hydras.Prelude.LibHyps_Experiments

From LibHyps Require Export LibHyps.
From hydras Require Export MoreLibHyps.


From Coq Require Import List.
Import ListNotations.
#[local] Open Scope autonaming_scope.

Ltac rename_hyp n th ::= rename_short n th.

Goal ∀ n p , n ≤ p → ∀ q, p ≤ q → n ≤ q.

Goal ∀ n p , n ≤ p → ∀ q, p ≤ q → n ≤ q.

From Coq Require Import Arith.
Parameters f g h : nat → nat.
Parameter P : nat→nat→nat→ Prop.
Goal ∀ x y , f (g (h x)) = h (g (f y)) → x = y → x < y →
                   P x y x → f y ≠ f x.