Commit 462ea92a authored by Robbert Krebbers's avatar Robbert Krebbers

Misc prelude omissions.

parent d101c562
......@@ -862,6 +862,9 @@ Instance idem_propholds {A} (R : relation A) f :
Idempotent R f x, PropHolds (R (f x x) x).
Proof. red. trivial. Qed.
Instance: `{R1 : relation A, R2 : relation B} (x : B),
Reflexive R2 Proper (R1 ==> R2) (λ _, x).
Proof. intros A R1 B R2 x ? y1 y2; reflexivity. Qed.
Instance: @PreOrder A (=).
Proof. split; repeat intro; congruence. Qed.
Lemma injective_iff {A B} {R : relation A} {S : relation B} (f : A B)
......
......@@ -11,6 +11,7 @@ Open Scope nat_scope.
Coercion Z.of_nat : nat >-> Z.
(** * Notations and properties of [nat] *)
Arguments minus !_ !_ /.
Reserved Notation "x ≤ y ≤ z" (at level 70, y at next level).
Reserved Notation "x ≤ y < z" (at level 70, y at next level).
Reserved Notation "x < y < z" (at level 70, y at next level).
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment