aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/closed/4763.v
blob: 9613b5c24891880385b96c7cd3d5c45fc374e484 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
Require Import Coq.Arith.Arith Coq.Classes.Morphisms Coq.Classes.RelationClasses.
Coercion is_true : bool >-> Sortclass.
Global Instance: Transitive leb.
Admitted.

Goal forall x y z, leb x y -> leb y z -> True.
  intros ??? H H'.
  lazymatch goal with
  | [ H : is_true (?R ?x ?y), H' : is_true (?R ?y ?z) |- _ ]
    => pose proof (transitivity H H' : is_true (R x z))
  end.
  exact I.
Qed.