diff --git a/theories/base.v b/theories/base.v
index 82c6b8d656a965d4b4ee50219c839d7663253dcb..24ea3864c93ce7c1a9d2a049854f7cf4265d437c 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -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)
diff --git a/theories/numbers.v b/theories/numbers.v
index f0f366a854251d021f7d362eefc8256cfbde17c5..d7d5ec961d24178f4a0d9f5bbabac13a39d149c6 100644
--- a/theories/numbers.v
+++ b/theories/numbers.v
@@ -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).