Add instances on int

math-comp · Nov 25, 2024 · ce41c55 · ce41c55
1 parent 6723e9b
commit ce41c55
Showing 1 changed file with 14 additions and 0 deletions.
diff --git a/reals/itv.v b/reals/itv.v
@@ -1371,6 +1371,20 @@ Canonical nat_min_max_typ :=
 
 End NatInstances.
 
+Section IntInstances.
+
+Lemma Posz_inum_subproof n : num_spec (Itv.Real `[0, +oo[) (Posz n).
+Proof. by apply/and3P; rewrite /= num_real !bnd_simp. Qed.
+
+Canonical Posz_inum n := Itv.mk (Posz_inum_subproof n).
+
+Lemma Negz_inum_subproof n : num_spec (Itv.Real `]-oo, -1]) (Negz n).
+Proof. by apply/and3P; rewrite /= num_real !bnd_simp. Qed.
+
+Canonical Negz_inum n := Itv.mk (Negz_inum_subproof n).
+
+End IntInstances.
+
 Section Morph.
 Context {R : numDomainType} {i : Itv.t}.
 Local Notation nR := (num_def R i).