diff --git a/Make b/Make
index bb8772e..33fe044 100644
--- a/Make
+++ b/Make
@@ -1,3 +1,4 @@
+theories/ssrZ.v
 theories/zify_ssreflect.v
 theories/zify_algebra.v
 theories/zify.v
diff --git a/README.md b/README.md
index f16b73f..d3d82ec 100644
--- a/README.md
+++ b/README.md
@@ -12,9 +12,9 @@ Follow the instructions on https://github.com/coq-community/templates to regener
 
 
 
-This small library enables the use of the Micromega tactics for goals stated
-with the definitions of the Mathematical Components library by extending the
-zify tactic.
+This small library enables the use of the Micromega arithmetic solvers of Coq
+for goals stated with the definitions of the Mathematical Components library
+by extending the zify tactic.
 
 ## Meta
 
@@ -47,4 +47,12 @@ make install
 ```
 
 
+## File contents
 
+- `zify_ssreflect.v`: Z-ification instances for the `coq-mathcomp-ssreflect`
+  library
+- `zify_algebra.v`: Z-ification instances for the `coq-mathcomp-algebra`
+  library
+- `zify.v`: re-exports all the Z-ification instances
+- `ssrZ.v`: provides a minimal facility for reasoning about `Z` and relating
+  `Z` and `int`
diff --git a/coq-mathcomp-zify.opam b/coq-mathcomp-zify.opam
index e8e42ce..a552965 100644
--- a/coq-mathcomp-zify.opam
+++ b/coq-mathcomp-zify.opam
@@ -12,9 +12,9 @@ license: "CECILL-B"
 
 synopsis: "Micromega tactics for Mathematical Components"
 description: """
-This small library enables the use of the Micromega tactics for goals stated
-with the definitions of the Mathematical Components library by extending the
-zify tactic."""
+This small library enables the use of the Micromega arithmetic solvers of Coq
+for goals stated with the definitions of the Mathematical Components library
+by extending the zify tactic."""
 
 build: [make "-j%{jobs}%" ]
 install: [make "install"]
diff --git a/meta.yml b/meta.yml
index c1ebe00..bb32d7f 100644
--- a/meta.yml
+++ b/meta.yml
@@ -9,9 +9,9 @@ synopsis: >-
   Micromega tactics for Mathematical Components
 
 description: |-
-  This small library enables the use of the Micromega tactics for goals stated
-  with the definitions of the Mathematical Components library by extending the
-  zify tactic.
+  This small library enables the use of the Micromega arithmetic solvers of Coq
+  for goals stated with the definitions of the Mathematical Components library
+  by extending the zify tactic.
 
 authors:
 - name: Kazuhiko Sakaguchi
@@ -51,4 +51,16 @@ dependencies:
     [MathComp](https://math-comp.github.io) 1.12.0 or later
 
 namespace: mathcomp.zify
+
+documentation: |-
+  ## File contents
+
+  - `zify_ssreflect.v`: Z-ification instances for the `coq-mathcomp-ssreflect`
+    library
+  - `zify_algebra.v`: Z-ification instances for the `coq-mathcomp-algebra`
+    library
+  - `zify.v`: re-exports all the Z-ification instances
+  - `ssrZ.v`: provides a minimal facility for reasoning about `Z` and relating
+    `Z` and `int`
+
 ---
diff --git a/theories/ssrZ.v b/theories/ssrZ.v
new file mode 100644
index 0000000..d6039d8
--- /dev/null
+++ b/theories/ssrZ.v
@@ -0,0 +1,169 @@
+From Coq Require Import ZArith ZifyClasses Zify ZifyInst ZifyBool.
+From Coq Require Export Lia.
+
+From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq path.
+From mathcomp Require Import div choice fintype tuple finfun bigop finset prime.
+From mathcomp Require Import order binomial ssralg countalg ssrnum ssrint.
+From mathcomp Require Import zify_ssreflect.
+
+Set Implicit Arguments.
+Unset Strict Implicit.
+Unset Printing Implicit Defensive.
+
+Import Order.Theory GRing.Theory Num.Theory.
+
+Definition int_of_Z (n : Z) : int :=
+  match n with
+  | Z0 => Posz 0
+  | Zpos p => Posz (Pos.to_nat p)
+  | Zneg p => Negz (Pos.to_nat p).-1
+  end.
+
+Definition Z_of_int (n : int) : Z :=
+  match n with
+  | Posz n => Z.of_nat n
+  | Negz n' => Z.opp (Z.of_nat (n' + 1))
+  end.
+
+Lemma int_of_ZK : cancel int_of_Z Z_of_int.
+Proof. by case=> //= p; lia. Qed.
+
+Lemma Z_of_intK : cancel Z_of_int int_of_Z.
+Proof.
+case=> [[|n]|n] //=.
+  congr Posz; lia.
+rewrite addnC /=; congr Negz; lia.
+Qed.
+
+Module ZInstances.
+
+Implicit Types (m n : Z).
+
+Fact eqZP : Equality.axiom Z.eqb.
+Proof. by move=> x y; apply: (iffP idP); lia. Qed.
+
+Canonical Z_eqType := EqType Z (EqMixin eqZP).
+Canonical Z_choiceType := ChoiceType Z (CanChoiceMixin int_of_ZK).
+Canonical Z_countType := CountType Z (CanCountMixin int_of_ZK).
+
+Definition Z_zmodMixin :=
+  ZmodMixin Zplus_assoc Zplus_comm Zplus_0_l Zplus_opp_l.
+Canonical Z_zmodType := ZmodType Z Z_zmodMixin.
+
+Definition Z_ringMixin :=
+  RingMixin
+    Zmult_assoc Zmult_1_l Zmult_1_r Zmult_plus_distr_l Zmult_plus_distr_r isT.
+Canonical Z_ringType := RingType Z Z_ringMixin.
+Canonical Z_comRingType := ComRingType Z Zmult_comm.
+
+Definition unitZ := [qualify a n : Z | (n == Z.pos xH) || (n == Z.neg xH)].
+Definition invZ n := n.
+
+Fact mulVZ : {in unitZ, left_inverse 1%R invZ *%R}.
+Proof. by move=> n /pred2P[] ->. Qed.
+
+Fact unitZPl m n : (n * m = 1)%R -> m \is a unitZ.
+Proof. case: m n => [|[m|m|]|[m|m|]] [|n|n] //= []; lia. Qed.
+
+Fact invZ_out : {in [predC unitZ], invZ =1 id}.
+Proof. exact. Qed.
+
+Fact idomain_axiomZ m n : (m * n = 0)%R -> (m == 0%R) || (n == 0%R).
+Proof. by case: m n => [|m|m] []. Qed.
+
+Canonical Z_unitRingType :=
+  UnitRingType Z (ComUnitRingMixin mulVZ unitZPl invZ_out).
+Canonical Z_comUnitRing := [comUnitRingType of Z].
+Canonical Z_idomainType := IdomainType Z idomain_axiomZ.
+
+Canonical Z_countZmodType := [countZmodType of Z].
+Canonical Z_countRingType := [countRingType of Z].
+Canonical Z_countComRingType := [countComRingType of Z].
+Canonical Z_countUnitRingType := [countUnitRingType of Z].
+Canonical Z_countComUnitRingType := [countComUnitRingType of Z].
+Canonical Z_countIdomainType := [countIdomainType of Z].
+
+Fact leZ_add m n : Z.leb 0 m -> Z.leb 0 n -> Z.leb 0 (m + n). Proof. lia. Qed.
+Fact leZ_mul m n : Z.leb 0 m -> Z.leb 0 n -> Z.leb 0 (m * n). Proof. lia. Qed.
+Fact leZ_anti m : Z.leb 0 m -> Z.leb m 0 -> m = Z0. Proof. lia. Qed.
+
+Fact subZ_ge0 m n : Z.leb 0 (n - m)%R = Z.leb m n.
+Proof. by rewrite /GRing.add /GRing.opp /=; lia. Qed.
+
+Fact leZ_total m n : Z.leb m n || Z.leb n m. Proof. lia. Qed.
+
+Fact normZN m : Z.abs (- m) = Z.abs m. Proof. lia. Qed.
+
+Fact geZ0_norm m : Z.leb 0 m -> Z.abs m = m. Proof. lia. Qed.
+
+Fact ltZ_def m n : (Z.ltb m n) = (n != m) && (Z.leb m n).
+Proof. by rewrite eqE /=; lia. Qed.
+
+Definition Mixin : realLeMixin [idomainType of Z] :=
+  RealLeMixin
+    leZ_add leZ_mul leZ_anti subZ_ge0 (leZ_total 0) normZN geZ0_norm ltZ_def.
+
+Canonical Z_porderType := POrderType ring_display Z Mixin.
+Canonical Z_latticeType := LatticeType Z Mixin.
+Canonical Z_distrLatticeType := DistrLatticeType Z Mixin.
+Canonical Z_orderType := OrderType Z leZ_total.
+Canonical Z_numDomainType := NumDomainType Z Mixin.
+Canonical Z_normedZmodType := NormedZmodType Z Z Mixin.
+Canonical Z_realDomainType := [realDomainType of Z].
+
+Fact Z_of_intE (n : int) : Z_of_int n = (n%:~R)%R.
+Proof.
+have Hnat (m : nat) : Z.of_nat m = (m%:R)%R.
+  by elim: m => // m; rewrite Nat2Z.inj_succ -Z.add_1_l mulrS => ->.
+case: n => n; rewrite /intmul /=; first exact: Hnat.
+by congr Z.opp; rewrite Nat2Z.inj_add /= mulrSr Hnat.
+Qed.
+
+Fact Z_of_int_is_additive : additive Z_of_int.
+Proof. by move=> m n; rewrite !Z_of_intE raddfB. Qed.
+
+Canonical Z_of_int_additive := Additive Z_of_int_is_additive.
+
+Fact int_of_Z_is_additive : additive int_of_Z.
+Proof. exact: can2_additive Z_of_intK int_of_ZK. Qed.
+
+Canonical int_of_Z_additive := Additive int_of_Z_is_additive.
+
+Fact Z_of_int_is_multiplicative : multiplicative Z_of_int.
+Proof. by split => // n m; rewrite !Z_of_intE rmorphM. Qed.
+
+Canonical Z_of_int_rmorphism := AddRMorphism Z_of_int_is_multiplicative.
+
+Fact int_of_Z_is_multiplicative : multiplicative int_of_Z.
+Proof. exact: can2_rmorphism Z_of_intK int_of_ZK. Qed.
+
+Canonical int_of_Z_rmorphism := AddRMorphism int_of_Z_is_multiplicative.
+
+End ZInstances.
+
+Canonical ZInstances.Z_eqType.
+Canonical ZInstances.Z_choiceType.
+Canonical ZInstances.Z_countType.
+Canonical ZInstances.Z_zmodType.
+Canonical ZInstances.Z_ringType.
+Canonical ZInstances.Z_comRingType.
+Canonical ZInstances.Z_unitRingType.
+Canonical ZInstances.Z_comUnitRing.
+Canonical ZInstances.Z_idomainType.
+Canonical ZInstances.Z_countZmodType.
+Canonical ZInstances.Z_countRingType.
+Canonical ZInstances.Z_countComRingType.
+Canonical ZInstances.Z_countUnitRingType.
+Canonical ZInstances.Z_countComUnitRingType.
+Canonical ZInstances.Z_countIdomainType.
+Canonical ZInstances.Z_porderType.
+Canonical ZInstances.Z_latticeType.
+Canonical ZInstances.Z_distrLatticeType.
+Canonical ZInstances.Z_orderType.
+Canonical ZInstances.Z_numDomainType.
+Canonical ZInstances.Z_normedZmodType.
+Canonical ZInstances.Z_realDomainType.
+Canonical ZInstances.Z_of_int_additive.
+Canonical ZInstances.int_of_Z_additive.
+Canonical ZInstances.Z_of_int_rmorphism.
+Canonical ZInstances.int_of_Z_rmorphism.
diff --git a/theories/zify_algebra.v b/theories/zify_algebra.v
index 64e835d..b21618e 100644
--- a/theories/zify_algebra.v
+++ b/theories/zify_algebra.v
@@ -5,7 +5,11 @@ From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq path.
 From mathcomp Require Import div choice fintype tuple finfun bigop finset prime.
 From mathcomp Require Import order binomial ssralg countalg ssrnum ssrint rat.
 From mathcomp Require Import intdiv.
-From mathcomp Require Import zify_ssreflect.
+From mathcomp Require Import zify_ssreflect ssrZ.
+
+Set Implicit Arguments.
+Unset Strict Implicit.
+Unset Printing Implicit Defensive.
 
 Module AlgebraZifyInstances.
 
@@ -17,50 +21,42 @@ Import Order.Theory GRing.Theory Num.Theory SsreflectZifyInstances.
 (* ssrint                                                                     *)
 (******************************************************************************)
 
-Definition Z_of_int (n : int) : Z :=
-  match n with
-  | Posz n => Z.of_nat n
-  | Negz n' => Z.opp (Z.of_nat (n' + 1))
-  end.
-
 Instance Inj_int_Z : InjTyp int Z :=
-  { inj := Z_of_int; pred := fun => True; cstr := fun => I }.
+  { inj := Z_of_int; pred _ := True; cstr _ := I }.
 Add Zify InjTyp Inj_int_Z.
 
-Instance Op_Z_of_int : UnOp Z_of_int := { TUOp := id; TUOpInj := fun => erefl }.
+Instance Op_Z_of_int : UnOp Z_of_int := { TUOp := id; TUOpInj _ := erefl }.
 Add Zify UnOp Op_Z_of_int.
 
-Instance Op_Posz : UnOp Posz := { TUOp := id; TUOpInj := fun => erefl }.
+Instance Op_int_of_Z : UnOp int_of_Z := { TUOp := id; TUOpInj := int_of_ZK }.
+Add Zify UnOp Op_int_of_Z.
+
+Instance Op_Posz : UnOp Posz := { TUOp := id; TUOpInj _ := erefl }.
 Add Zify UnOp Op_Posz.
 
 Instance Op_Negz : UnOp Negz :=
-  { TUOp := fun x => (- (x + 1))%Z; TUOpInj := ltac:(simpl; lia) }.
+  { TUOp x := (- (x + 1))%Z; TUOpInj := ltac:(simpl; lia) }.
 Add Zify UnOp Op_Negz.
 
-Lemma Op_int_eq_subproof n m : n = m <-> Z_of_int n = Z_of_int m.
-Proof. split=> [->|] //; case: n m => ? [] ? ?; f_equal; lia. Qed.
-
 Instance Op_int_eq : BinRel (@eq int) :=
-  { TR := @eq Z; TRInj := Op_int_eq_subproof }.
+  { TR := @eq Z; TRInj := ltac:(by split=> [->|/(can_inj Z_of_intK)]) }.
 Add Zify BinRel Op_int_eq.
 
 Instance Op_int_eq_op : BinOp (@eq_op int_eqType : int -> int -> bool) :=
   { TBOp := Z.eqb;
-    TBOpInj := ltac:(move=> [] ? [] ?; do 2 rewrite /eq_op /=; lia) }.
+    TBOpInj := ltac:(move=> [] ? [] ?; do 2 rewrite eqE /=; lia) }.
 Add Zify BinOp Op_int_eq_op.
 
 Instance Op_int_0 : CstOp (0%R : int) := { TCst := 0%Z; TCstInj := erefl }.
 Add Zify CstOp Op_int_0.
 
-Instance Op_addz : BinOp intZmod.addz :=
-  { TBOp := Z.add; TBOpInj := ltac:(case=> ? [] ? /=; try case: leqP; lia) }.
+Instance Op_addz : BinOp intZmod.addz := { TBOp := Z.add; TBOpInj := raddfD _ }.
 Add Zify BinOp Op_addz.
 
 Instance Op_int_add : BinOp +%R := Op_addz.
 Add Zify BinOp Op_int_add.
 
-Instance Op_oppz : UnOp intZmod.oppz :=
-  { TUOp := Z.opp; TUOpInj := ltac:(case=> [[|?]|?] /=; lia) }.
+Instance Op_oppz : UnOp intZmod.oppz := { TUOp := Z.opp; TUOpInj := raddfN _ }.
 Add Zify UnOp Op_oppz.
 
 Instance Op_int_opp : UnOp (@GRing.opp _) := Op_oppz.
@@ -70,27 +66,25 @@ Instance Op_int_1 : CstOp (1%R : int) := { TCst := 1%Z; TCstInj := erefl }.
 Add Zify CstOp Op_int_1.
 
 Instance Op_mulz : BinOp intRing.mulz :=
-  { TBOp := Z.mul; TBOpInj := ltac:(case=> ? [] ? /=; lia) }.
+  { TBOp := Z.mul; TBOpInj := rmorphM _ }.
 Add Zify BinOp Op_mulz.
 
 Instance Op_int_mulr : BinOp *%R := Op_mulz.
 Add Zify BinOp Op_int_mulr.
 
-Instance Op_int_intmul : BinOp ( *~%R%R : int -> int -> int) :=
-  { TBOp := Z.mul; TBOpInj := ltac:(move=> ? ?; rewrite /= mulrzz; lia) }.
-Add Zify BinOp Op_int_intmul.
-
 Instance Op_int_natmul : BinOp (@GRing.natmul _ : int -> nat -> int) :=
-  { TBOp := Z.mul;
-    TBOpInj := ltac:(move=> ? ?; rewrite /= pmulrn mulrzz; lia) }.
+  { TBOp := Z.mul; TBOpInj _ _ := ltac:(rewrite /= pmulrn mulrzz; lia) }.
 Add Zify BinOp Op_int_natmul.
 
+Instance Op_int_intmul : BinOp ( *~%R%R : int -> int -> int) :=
+  { TBOp := Z.mul; TBOpInj _ _ := ltac:(rewrite /= mulrzz; lia) }.
+Add Zify BinOp Op_int_intmul.
+
 Instance Op_int_scale : BinOp (@GRing.scale _ [lmodType int of int^o]) :=
   Op_mulz.
 Add Zify BinOp Op_int_scale.
 
-Lemma Op_int_exp_subproof n m :
-  Z_of_int (n ^+ m) = (Z_of_int n ^ Z.of_nat m)%Z.
+Fact Op_int_exp_subproof n m : Z_of_int (n ^+ m) = (Z_of_int n ^ Z.of_nat m)%Z.
 Proof. rewrite -Zpower_nat_Z; elim: m => //= m <-; rewrite exprS; lia. Qed.
 
 Instance Op_int_exp : BinOp (@GRing.exp _ : int -> nat -> int) :=
@@ -98,7 +92,7 @@ Instance Op_int_exp : BinOp (@GRing.exp _ : int -> nat -> int) :=
 Add Zify BinOp Op_int_exp.
 
 Instance Op_invz : UnOp intUnitRing.invz :=
-  { TUOp := id; TUOpInj := fun => erefl }.
+  { TUOp := id; TUOpInj _ := erefl }.
 Add Zify UnOp Op_invz.
 
 Instance Op_int_inv : UnOp GRing.inv := Op_invz.
@@ -154,40 +148,159 @@ Instance Op_int_gt' : BinOp (<^d%O : rel int^d) := Op_int_gt.
 Add Zify BinOp Op_int_gt'.
 
 Instance Op_int_min : BinOp (Order.min : int -> int -> int) :=
-  { TBOp := Z.min; TBOpInj := ltac:(move=> ? ? /=; case: leP; lia) }.
+  { TBOp := Z.min; TBOpInj _ _ := ltac:(case: leP => /=; lia) }.
 Add Zify BinOp Op_int_min.
 
 Instance Op_int_min' : BinOp ((Order.max : int^d -> _) : int -> int -> int) :=
-  { TBOp := Z.min; TBOpInj := ltac:(move=> ? ? /=; case: leP; lia) }.
+  { TBOp := Z.min; TBOpInj _ _ := ltac:(case: leP => /=; lia) }.
 Add Zify BinOp Op_int_min'.
 
 Instance Op_int_max : BinOp (Order.max : int -> int -> int) :=
-  { TBOp := Z.max; TBOpInj := ltac:(move=> ? ? /=; case: leP; lia) }.
+  { TBOp := Z.max; TBOpInj _ _ := ltac:(case: leP => /=; lia) }.
 Add Zify BinOp Op_int_max.
 
 Instance Op_int_max' : BinOp ((Order.min : int^d -> _) : int -> int -> int) :=
-  { TBOp := Z.max; TBOpInj := ltac:(move=> ? ? /=; case: leP; lia) }.
+  { TBOp := Z.max; TBOpInj _ _ := ltac:(case: leP => /=; lia) }.
 Add Zify BinOp Op_int_max'.
 
 Instance Op_int_meet : BinOp (Order.meet : int -> int -> int) :=
-  { TBOp := Z.min; TBOpInj := ltac:(move=> ? ? /=; case: leP; lia) }.
+  { TBOp := Z.min; TBOpInj _ _ := ltac:(case: leP => /=; lia) }.
 Add Zify BinOp Op_int_meet.
 
 Instance Op_int_meet' : BinOp (Order.join : int^d -> _) := Op_int_min.
 Add Zify BinOp Op_int_meet'.
 
 Instance Op_int_join : BinOp (Order.join : int -> int -> int) :=
-  { TBOp := Z.max; TBOpInj := ltac:(move=> ? ? /=; case: leP; lia) }.
+  { TBOp := Z.max; TBOpInj _ _ := ltac:(case: leP => /=; lia) }.
 Add Zify BinOp Op_int_join.
 
 Instance Op_int_join' : BinOp (Order.meet : int^d -> _) := Op_int_max.
 Add Zify BinOp Op_int_join'.
 
+(******************************************************************************)
+(* ssrZ                                                                       *)
+(******************************************************************************)
+
+Instance Op_Z_eq_op : BinOp (eq_op : Z -> Z -> bool) := Op_Zeqb.
+Add Zify BinOp Op_Z_eq_op.
+
+Instance Op_Z_0 : CstOp (0%R : Z) := { TCst := 0%Z; TCstInj := erefl }.
+Add Zify CstOp Op_Z_0.
+
+Instance Op_Z_add : BinOp (+%R : Z -> Z -> Z) :=
+  { TBOp := Z.add; TBOpInj _ _ := erefl }.
+Add Zify BinOp Op_Z_add.
+
+Instance Op_Z_opp : UnOp (@GRing.opp _ : Z -> Z) :=
+  { TUOp := Z.opp; TUOpInj _ := erefl }.
+Add Zify UnOp Op_Z_opp.
+
+Instance Op_Z_1 : CstOp (1%R : Z) := { TCst := 1%Z; TCstInj := erefl }.
+Add Zify CstOp Op_Z_1.
+
+Instance Op_Z_mulr : BinOp ( *%R : Z -> Z -> Z) :=
+  { TBOp := Z.mul; TBOpInj _ _ := erefl }.
+Add Zify BinOp Op_Z_mulr.
+
+Fact Op_Z_natmul_subproof (n : Z) (m : nat) : (n *+ m)%R = (n * Z.of_nat m)%Z.
+Proof. elim: m => [|m]; rewrite (mulr0n, mulrS); lia. Qed.
+
+Instance Op_Z_natmul : BinOp (@GRing.natmul _ : Z -> nat -> Z) :=
+  { TBOp := Z.mul; TBOpInj := Op_Z_natmul_subproof }.
+Add Zify BinOp Op_Z_natmul.
+
+Instance Op_Z_intmul : BinOp ( *~%R%R : Z -> int -> Z) :=
+  { TBOp := Z.mul; TBOpInj := ltac:(move=> n [] m; rewrite /intmul /=; lia) }.
+Add Zify BinOp Op_Z_intmul.
+
+Instance Op_Z_scale : BinOp (@GRing.scale _ [lmodType Z of Z^o]) := Op_Z_mulr.
+Add Zify BinOp Op_Z_scale.
+
+Fact Op_Z_exp_subproof n m : (n ^+ m)%R = (n ^ Z.of_nat m)%Z.
+Proof. by rewrite -Zpower_nat_Z; elim: m => //= m <-; rewrite exprS. Qed.
+
+Instance Op_Z_exp : BinOp (@GRing.exp _ : Z -> nat -> Z) :=
+  { TBOp := Z.pow; TBOpInj := Op_Z_exp_subproof }.
+Add Zify BinOp Op_Z_exp.
+
+Instance Op_invZ : UnOp ZInstances.invZ := { TUOp := id; TUOpInj _ := erefl }.
+Add Zify UnOp Op_invZ.
+
+Instance Op_Z_inv : UnOp (GRing.inv : Z -> Z) :=
+  { TUOp := id; TUOpInj _ := erefl }.
+Add Zify UnOp Op_Z_inv.
+
+Instance Op_Z_normr : UnOp (Num.norm : Z -> Z) :=
+  { TUOp := Z.abs; TUOpInj _ := erefl }.
+Add Zify UnOp Op_Z_normr.
+
+Instance Op_Z_sgr : UnOp (Num.sg : Z -> Z) :=
+  { TUOp := Z.sgn; TUOpInj := ltac:(case=> //=; lia) }.
+Add Zify UnOp Op_Z_sgr.
+
+Instance Op_Z_le : BinOp (<=%O : Z -> Z -> bool) :=
+  { TBOp := Z.leb; TBOpInj _ _ := erefl }.
+Add Zify BinOp Op_Z_le.
+
+Instance Op_Z_le' : BinOp (>=^d%O : rel Z^d) := Op_Z_le.
+Add Zify BinOp Op_Z_le'.
+
+Instance Op_Z_ge : BinOp (>=%O : Z -> Z -> bool) :=
+  { TBOp := Z.geb; TBOpInj := ltac:(simpl; lia) }.
+Add Zify BinOp Op_Z_ge.
+
+Instance Op_Z_ge' : BinOp (<=^d%O : rel Z^d) := Op_Z_ge.
+Add Zify BinOp Op_Z_ge'.
+
+Instance Op_Z_lt : BinOp (<%O : Z -> Z -> bool) :=
+  { TBOp := Z.ltb; TBOpInj _ _ := erefl }.
+Add Zify BinOp Op_Z_lt.
+
+Instance Op_Z_lt' : BinOp (>^d%O : rel Z^d) := Op_Z_lt.
+Add Zify BinOp Op_Z_lt'.
+
+Instance Op_Z_gt : BinOp (>%O : Z -> Z -> bool) :=
+  { TBOp := Z.gtb; TBOpInj := ltac:(simpl; lia) }.
+Add Zify BinOp Op_Z_gt.
+
+Instance Op_Z_gt' : BinOp (<^d%O : rel Z^d) := Op_Z_gt.
+Add Zify BinOp Op_Z_gt'.
+
+Instance Op_Z_min : BinOp (Order.min : Z -> Z -> Z) :=
+  { TBOp := Z.min; TBOpInj _ _ := ltac:(case: leP => /=; lia) }.
+Add Zify BinOp Op_Z_min.
+
+Instance Op_Z_min' : BinOp ((Order.max : Z^d -> _) : Z -> Z -> Z) :=
+  { TBOp := Z.min; TBOpInj _ _ := ltac:(case: leP => /=; lia) }.
+Add Zify BinOp Op_Z_min'.
+
+Instance Op_Z_max : BinOp (Order.max : Z -> Z -> Z) :=
+  { TBOp := Z.max; TBOpInj _ _ := ltac:(case: leP => /=; lia) }.
+Add Zify BinOp Op_Z_max.
+
+Instance Op_Z_max' : BinOp ((Order.min : Z^d -> _) : Z -> Z -> Z) :=
+  { TBOp := Z.max; TBOpInj _ _ := ltac:(case: leP => /=; lia) }.
+Add Zify BinOp Op_Z_max'.
+
+Instance Op_Z_meet : BinOp (Order.meet : Z -> Z -> Z) :=
+  { TBOp := Z.min; TBOpInj _ _ := ltac:(case: leP => /=; lia) }.
+Add Zify BinOp Op_Z_meet.
+
+Instance Op_Z_meet' : BinOp (Order.join : Z^d -> _) := Op_Z_min.
+Add Zify BinOp Op_Z_meet'.
+
+Instance Op_Z_join : BinOp (Order.join : Z -> Z -> Z) :=
+  { TBOp := Z.max; TBOpInj _ _ := ltac:(case: leP => /=; lia) }.
+Add Zify BinOp Op_Z_join.
+
+Instance Op_Z_join' : BinOp (Order.meet : Z^d -> _) := Op_Z_max.
+Add Zify BinOp Op_Z_join'.
+
 (******************************************************************************)
 (* intdiv                                                                     *)
 (******************************************************************************)
 
-Lemma Op_divz_subproof n m :
+Fact Op_divz_subproof n m :
   Z_of_int (divz n m) = divZ (Z_of_int n) (Z_of_int m).
 Proof. case: n => [[|n]|n]; rewrite /divz /divZ /= ?addn1 /=; nia. Qed.
 
@@ -200,11 +313,11 @@ Instance Op_modz : BinOp modz :=
 Add Zify BinOp Op_modz.
 
 Instance Op_dvdz : BinOp dvdz :=
-  { TBOp := fun n m => Z.eqb (modZ m n) 0%Z;
-    TBOpInj := ltac:(move=> ? ? /=; apply/dvdz_mod0P/idP; lia) }.
+  { TBOp n m := Z.eqb (modZ m n) 0%Z;
+    TBOpInj _ _ := ltac:(apply/dvdz_mod0P/idP; lia) }.
 Add Zify BinOp Op_dvdz.
 
-Lemma Op_gcdz_subproof n m :
+Fact Op_gcdz_subproof n m :
   Z_of_int (gcdz n m) = Z.gcd (Z_of_int n) (Z_of_int m).
 Proof. rewrite /gcdz -Z.gcd_abs_l -Z.gcd_abs_r; lia. Qed.
 
@@ -212,7 +325,7 @@ Instance Op_gcdz : BinOp gcdz := { TBOp := Z.gcd; TBOpInj := Op_gcdz_subproof }.
 Add Zify BinOp Op_gcdz.
 
 Instance Op_coprimez : BinOp coprimez :=
-  { TBOp := fun x y => Z.eqb (Z.gcd x y) 1%Z;
+  { TBOp x y := Z.eqb (Z.gcd x y) 1%Z;
     TBOpInj := ltac:(rewrite /= /coprimez; lia) }.
 Add Zify BinOp Op_coprimez.
 
@@ -231,8 +344,8 @@ Add Zify UnOp Op_int_opp.
 Add Zify CstOp Op_int_1.
 Add Zify BinOp Op_mulz.
 Add Zify BinOp Op_int_mulr.
-Add Zify BinOp Op_int_intmul.
 Add Zify BinOp Op_int_natmul.
+Add Zify BinOp Op_int_intmul.
 Add Zify BinOp Op_int_scale.
 Add Zify BinOp Op_int_exp.
 Add Zify UnOp Op_invz.
@@ -259,6 +372,36 @@ Add Zify BinOp Op_int_meet.
 Add Zify BinOp Op_int_meet'.
 Add Zify BinOp Op_int_join.
 Add Zify BinOp Op_int_join'.
+Add Zify BinOp Op_Z_eq_op.
+Add Zify CstOp Op_Z_0.
+Add Zify BinOp Op_Z_add.
+Add Zify UnOp Op_Z_opp.
+Add Zify CstOp Op_Z_1.
+Add Zify BinOp Op_Z_mulr.
+Add Zify BinOp Op_Z_natmul.
+Add Zify BinOp Op_Z_intmul.
+Add Zify BinOp Op_Z_scale.
+Add Zify BinOp Op_Z_exp.
+Add Zify UnOp Op_invZ.
+Add Zify UnOp Op_Z_inv.
+Add Zify UnOp Op_Z_normr.
+Add Zify UnOp Op_Z_sgr.
+Add Zify BinOp Op_Z_le.
+Add Zify BinOp Op_Z_le'.
+Add Zify BinOp Op_Z_ge.
+Add Zify BinOp Op_Z_ge'.
+Add Zify BinOp Op_Z_lt.
+Add Zify BinOp Op_Z_lt'.
+Add Zify BinOp Op_Z_gt.
+Add Zify BinOp Op_Z_gt'.
+Add Zify BinOp Op_Z_min.
+Add Zify BinOp Op_Z_min'.
+Add Zify BinOp Op_Z_max.
+Add Zify BinOp Op_Z_max'.
+Add Zify BinOp Op_Z_meet.
+Add Zify BinOp Op_Z_meet'.
+Add Zify BinOp Op_Z_join.
+Add Zify BinOp Op_Z_join'.
 Add Zify BinOp Op_divz.
 Add Zify BinOp Op_modz.
 Add Zify BinOp Op_dvdz.
diff --git a/theories/zify_ssreflect.v b/theories/zify_ssreflect.v
index 021fa1b..6471b1d 100644
--- a/theories/zify_ssreflect.v
+++ b/theories/zify_ssreflect.v
@@ -16,7 +16,7 @@ Module SsreflectZifyInstances.
 Import Order.Theory.
 
 Instance Op_bool_inj : UnOp (inj : bool -> bool) :=
-  { TUOp := id; TUOpInj := fun => erefl }.
+  { TUOp := id; TUOpInj _ := erefl }.
 Add Zify UnOp Op_bool_inj.
 
 Instance Op_nat_inj : UnOp (inj : nat -> Z) := Op_Z_of_nat.
@@ -27,7 +27,7 @@ Add Zify UnOp Op_nat_inj.
 (******************************************************************************)
 
 Instance Op_addb : BinOp addb :=
-  { TBOp := fun x y => Bool.eqb x (negb y); TBOpInj := ltac:(by case=> [][]) }.
+  { TBOp x y := Bool.eqb x (negb y); TBOpInj := ltac:(by case=> [][]) }.
 Add Zify BinOp Op_addb.
 
 Instance Op_eqb : BinOp eqb :=
@@ -45,21 +45,21 @@ Instance Op_bool_le' : BinOp (>=^d%O : rel bool^d) := Op_bool_le.
 Add Zify BinOp Op_bool_le'.
 
 Instance Op_bool_ge : BinOp (>=%O : bool -> bool -> bool) :=
-  { TBOp := fun x y => implb y x; TBOpInj := ltac:(by case=> [][]) }.
+  { TBOp x y := implb y x; TBOpInj := ltac:(by case=> [][]) }.
 Add Zify BinOp Op_bool_ge.
 
 Instance Op_bool_ge' : BinOp (<=^d%O : rel bool^d) := Op_bool_ge.
 Add Zify BinOp Op_bool_ge'.
 
 Instance Op_bool_lt : BinOp (<%O : bool -> bool -> bool) :=
-  { TBOp := fun x y => ~~ x && y; TBOpInj := ltac:(by case=> [][]) }.
+  { TBOp x y := ~~ x && y; TBOpInj := ltac:(by case=> [][]) }.
 Add Zify BinOp Op_bool_lt.
 
 Instance Op_bool_lt' : BinOp (>^d%O : rel bool^d) := Op_bool_lt.
 Add Zify BinOp Op_bool_lt'.
 
 Instance Op_bool_gt : BinOp (>%O : bool -> bool -> bool) :=
-  { TBOp := fun x y => x && ~~ y; TBOpInj := ltac:(by case=> [][]) }.
+  { TBOp x y := x && ~~ y; TBOpInj := ltac:(by case=> [][]) }.
 Add Zify BinOp Op_bool_gt.
 
 Instance Op_bool_gt' : BinOp (<^d%O : rel bool^d) := Op_bool_gt.
@@ -108,7 +108,7 @@ Instance Op_bool_top' : CstOp (0%O : bool^d) := Op_true.
 Add Zify CstOp Op_bool_top'.
 
 Instance Op_bool_sub : BinOp (Order.sub : bool -> bool -> bool) :=
-  { TBOp := fun x y => x && ~~ y; TBOpInj := ltac:(by case=> [][]) }.
+  { TBOp x y := x && ~~ y; TBOpInj := ltac:(by case=> [][]) }.
 Add Zify BinOp Op_bool_sub.
 
 Instance Op_bool_compl : UnOp (Order.compl : bool -> bool) := Op_negb.
@@ -159,11 +159,11 @@ Instance Op_gtn : BinOp (gtn : nat -> nat -> bool) :=
 Add Zify BinOp Op_gtn.
 
 Instance Op_minn : BinOp minn :=
-  { TBOp := Z.min; TBOpInj := ltac:(move=> ? ?; case: leqP; lia) }.
+  { TBOp := Z.min; TBOpInj _ _ := ltac:(case: leqP; lia) }.
 Add Zify BinOp Op_minn.
 
 Instance Op_maxn : BinOp maxn :=
-  { TBOp := Z.max; TBOpInj := ltac:(move=> ? ?; case: leqP; lia) }.
+  { TBOp := Z.max; TBOpInj _ _ := ltac:(case: leqP; lia) }.
 Add Zify BinOp Op_maxn.
 
 Instance Op_nat_of_bool : UnOp nat_of_bool :=
@@ -171,10 +171,10 @@ Instance Op_nat_of_bool : UnOp nat_of_bool :=
 Add Zify UnOp Op_nat_of_bool.
 
 Instance Op_double : UnOp double :=
-  { TUOp := Z.mul 2; TUOpInj := ltac:(move=> ?; rewrite -muln2; lia) }.
+  { TUOp := Z.mul 2; TUOpInj _ := ltac:(rewrite -muln2; lia) }.
 Add Zify UnOp Op_double.
 
-Lemma Op_expn_subproof n m : Z.of_nat (n ^ m) = (Z.of_nat n ^ Z.of_nat m)%Z.
+Fact Op_expn_subproof n m : Z.of_nat (n ^ m) = (Z.of_nat n ^ Z.of_nat m)%Z.
 Proof. rewrite -Zpower_nat_Z; elim: m => //= m <-; rewrite expnS; lia. Qed.
 
 Instance Op_expn_rec : BinOp expn_rec :=
@@ -212,14 +212,14 @@ Instance Op_nat_min : BinOp (Order.min : nat -> _) := Op_minn.
 Add Zify BinOp Op_nat_min.
 
 Instance Op_nat_min' : BinOp ((Order.max : nat^d -> _) : nat -> nat -> nat) :=
-  { TBOp := Z.min; TBOpInj := ltac:(move=> ? ? /=; case: leP; lia) }.
+  { TBOp := Z.min; TBOpInj _ _ := ltac:(case: leP; lia) }.
 Add Zify BinOp Op_nat_min'.
 
 Instance Op_nat_max : BinOp (Order.max : nat -> _) := Op_maxn.
 Add Zify BinOp Op_nat_max.
 
 Instance Op_nat_max' : BinOp ((Order.min : nat^d -> _) : nat -> nat -> nat) :=
-  { TBOp := Z.max; TBOpInj := ltac:(move=> ? ? /=; case: leP; lia) }.
+  { TBOp := Z.max; TBOpInj _ _ := ltac:(case: leP; lia) }.
 Add Zify BinOp Op_nat_max'.
 
 Instance Op_nat_meet : BinOp (Order.meet : nat -> _) := Op_minn.
@@ -254,39 +254,39 @@ Definition divZ (m d : Z) : Z :=
 
 Definition modZ (m d : Z) : Z := (m - divZ m d * d)%Z.
 
-Instance Op_divZ : BinOp divZ := { TBOp := divZ; TBOpInj := fun _ _ => erefl }.
+Instance Op_divZ : BinOp divZ := { TBOp := divZ; TBOpInj _ _ := erefl }.
 Add Zify BinOp Op_divZ.
 
-Instance Op_modZ : BinOp modZ := { TBOp := modZ; TBOpInj := fun _ _ => erefl }.
+Instance Op_modZ : BinOp modZ := { TBOp := modZ; TBOpInj _ _ := erefl }.
 Add Zify BinOp Op_modZ.
 
 (* Reimplementation of Z.div_mod_to_equations (PreOmega.v) for divZ and modZ: *)
 
-Lemma divZ_eq m d : m = (divZ m d * d + modZ m d)%Z.
+Fact divZ_eq m d : m = (divZ m d * d + modZ m d)%Z.
 Proof. rewrite /modZ; lia. Qed.
 
-Lemma modZ_ge0 m d : d <> 0%Z -> (0 <= modZ m d)%Z.
+Fact modZ_ge0 m d : d <> 0%Z -> (0 <= modZ m d)%Z.
 Proof.
 by move: d m => [] // d [] // m _; rewrite /modZ /divZ [Z.abs_nat _]/=;
   move: (leq_trunc_div (Pos.to_nat m) (Pos.to_nat d));
   move: (@ltn_ceil (Pos.to_nat m).-1 (Pos.to_nat d)); lia.
 Qed.
 
-Lemma ltz_pmodZ m d : (0 < d)%Z -> (modZ m d < d)%Z.
+Fact ltz_pmodZ m d : (0 < d)%Z -> (modZ m d < d)%Z.
 Proof.
 by move: d m => [] // d [] // m _; rewrite /modZ /divZ [Z.abs_nat _]/=;
   move: (leq_trunc_div (Pos.to_nat m).-1 (Pos.to_nat d));
   move: (@ltn_ceil (Pos.to_nat m) (Pos.to_nat d)); lia.
 Qed.
 
-Lemma ltz_nmodZ m d : (d < 0)%Z -> (modZ m d < - d)%Z.
+Fact ltz_nmodZ m d : (d < 0)%Z -> (modZ m d < - d)%Z.
 Proof.
 move: d m => [] // d [] // m _; rewrite /modZ /divZ [Z.abs_nat _]/=;
   move: (leq_trunc_div (Pos.to_nat m).-1 (Pos.to_nat d));
   move: (@ltn_ceil (Pos.to_nat m) (Pos.to_nat d)); lia.
 Qed.
 
-Lemma divZ0 m d : d = 0%Z -> divZ m d = 0%Z.
+Fact divZ0 m d : d = 0%Z -> divZ m d = 0%Z.
 Proof. by move=> ->. Qed.
 
 Ltac divZ_modZ_to_equations :=
@@ -325,7 +325,7 @@ Ltac Zify.zify_post_hook ::= elim_bool_cstr; divZ_modZ_to_equations.
 (* div (divn, modn, dvdn, gcdn, lcmn, and coprime)                            *)
 (******************************************************************************)
 
-Lemma Op_divn_subproof n m : Z.of_nat (n %/ m) = divZ (Z.of_nat n) (Z.of_nat m).
+Fact Op_divn_subproof n m : Z.of_nat (n %/ m) = divZ (Z.of_nat n) (Z.of_nat m).
 Proof.
 by case: n m => [|n] [|m]; rewrite /divZ //= ?SuccNat2Pos.id_succ; case: divn.
 Qed.
@@ -334,30 +334,28 @@ Instance Op_divn : BinOp divn := { TBOp := divZ; TBOpInj := Op_divn_subproof }.
 Add Zify BinOp Op_divn.
 
 Instance Op_modn : BinOp modn :=
-  { TBOp := modZ; TBOpInj := ltac:(move=> n m; move: (divn_eq n m); lia) }.
+  { TBOp := modZ; TBOpInj n m := ltac:(move: (divn_eq n m); lia) }.
 Add Zify BinOp Op_modn.
 
 Instance Op_dvdn : BinOp dvdn :=
-  { TBOp := fun x y => Z.eqb (modZ y x) 0%Z;
+  { TBOp x y := Z.eqb (modZ y x) 0%Z;
     TBOpInj := ltac:(rewrite /dvdn; lia) }.
 Add Zify BinOp Op_dvdn.
 
 Instance Op_odd : UnOp odd :=
-  { TUOp := fun x => Z.eqb (modZ x 2) 1%Z;
-    TUOpInj := ltac:(move=> n; case: odd (modn2 n); lia) }.
+  { TUOp x := Z.eqb (modZ x 2) 1%Z;
+    TUOpInj n := ltac:(case: odd (modn2 n); lia) }.
 Add Zify UnOp Op_odd.
 
 Instance Op_half : UnOp half :=
-  { TUOp := fun x => divZ x 2;
-    TUOpInj := ltac:(move=> ?; rewrite -divn2; lia) }.
+  { TUOp x := divZ x 2; TUOpInj _ := ltac:(rewrite -divn2; lia) }.
 Add Zify UnOp Op_half.
 
 Instance Op_uphalf : UnOp uphalf :=
-  { TUOp := fun x => divZ (x + 1)%Z 2;
-    TUOpInj := ltac:(move=> ?; rewrite uphalf_half; lia) }.
+  { TUOp x := divZ (x + 1)%Z 2; TUOpInj _ := ltac:(rewrite uphalf_half; lia) }.
 Add Zify UnOp Op_uphalf.
 
-Lemma Op_gcdn_subproof n m :
+Fact Op_gcdn_subproof n m :
   Z.of_nat (gcdn n m) = Z.gcd (Z.of_nat n) (Z.of_nat m).
 Proof.
 apply/esym/Z.gcd_unique; first by case: gcdn.
@@ -373,7 +371,7 @@ Qed.
 Instance Op_gcdn : BinOp gcdn := { TBOp := Z.gcd; TBOpInj := Op_gcdn_subproof }.
 Add Zify BinOp Op_gcdn.
 
-Lemma Op_lcmn_subproof n m :
+Fact Op_lcmn_subproof n m :
   Z.of_nat (lcmn n m) = Z.lcm (Z.of_nat n) (Z.of_nat m).
 Proof.
 case: n m => [|n][|m]; rewrite ?lcmn0 // /lcmn /Z.lcm -Op_gcdn_subproof.
@@ -386,7 +384,7 @@ Instance Op_lcmn : BinOp lcmn := { TBOp := Z.lcm; TBOpInj := Op_lcmn_subproof }.
 Add Zify BinOp Op_lcmn.
 
 Instance Op_coprime : BinOp coprime :=
-  { TBOp := fun x y => Z.eqb (Z.gcd x y) 1%Z;
+  { TBOp x y := Z.eqb (Z.gcd x y) 1%Z;
     TBOpInj := ltac:(rewrite /= /coprime; lia) }.
 Add Zify BinOp Op_coprime.
 
@@ -401,23 +399,23 @@ Instance Op_natdvd_le' : BinOp (>=^d%O : rel natdvd^d) := Op_dvdn.
 Add Zify BinOp Op_natdvd_le'.
 
 Instance Op_natdvd_ge : BinOp ((>=%O : rel natdvd) : nat -> nat -> bool) :=
-  { TBOp := fun x y => Z.eqb (modZ x y) 0%Z; TBOpInj := ltac:(simpl; lia) }.
+  { TBOp x y := Z.eqb (modZ x y) 0%Z; TBOpInj := ltac:(simpl; lia) }.
 Add Zify BinOp Op_natdvd_ge.
 
 Instance Op_natdvd_ge' : BinOp (<=^d%O : rel natdvd^d) := Op_natdvd_ge.
 Add Zify BinOp Op_natdvd_ge'.
 
 Instance Op_natdvd_lt : BinOp ((<%O : rel natdvd) : nat -> nat -> bool) :=
-  { TBOp := fun x y => negb (Z.eqb y x) && Z.eqb (modZ y x) 0%Z;
-    TBOpInj := ltac:(move=> ? ? /=; rewrite sdvdEnat; lia) }.
+  { TBOp x y := negb (Z.eqb y x) && Z.eqb (modZ y x) 0%Z;
+    TBOpInj _ _ := ltac:(rewrite /= sdvdEnat; lia) }.
 Add Zify BinOp Op_natdvd_lt.
 
 Instance Op_natdvd_lt' : BinOp (>^d%O : rel natdvd^d) := Op_natdvd_lt.
 Add Zify BinOp Op_natdvd_lt'.
 
 Instance Op_natdvd_gt : BinOp ((>%O : rel natdvd) : nat -> nat -> bool) :=
-  { TBOp := fun x y => negb (Z.eqb x y) && Z.eqb (modZ x y) 0%Z;
-    TBOpInj := ltac:(move=> ? ? /=; rewrite sdvdEnat; lia) }.
+  { TBOp x y := negb (Z.eqb x y) && Z.eqb (modZ x y) 0%Z;
+    TBOpInj _ _ := ltac:(rewrite /= sdvdEnat; lia) }.
 Add Zify BinOp Op_natdvd_gt.
 
 Instance Op_natdvd_gt' : BinOp (<^d%O : rel natdvd^d) := Op_natdvd_gt.