blob: ae8ed0e6e8bd5dd9bdea1739ebe50f1d8ae7b1c8 (
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.
|
