From 76adb57c72fccb4f3e416bd7f3927f4fff72178b Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 1 Jun 2014 10:26:26 +0200
Subject: Making those proofs which depend on names generated for the arguments
 in Prop of constructors of inductive types independent of these names.

Incidentally upgraded/simplified a couple of proofs, mainly in Reals.

This prepares to the next commit about using names based on H for such
hypotheses in Prop.
---
 theories/Numbers/Cyclic/ZModulo/ZModulo.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'theories/Numbers/Cyclic/ZModulo')

diff --git a/theories/Numbers/Cyclic/ZModulo/ZModulo.v b/theories/Numbers/Cyclic/ZModulo/ZModulo.v
index 334836954b..dbc7582d50 100644
--- a/theories/Numbers/Cyclic/ZModulo/ZModulo.v
+++ b/theories/Numbers/Cyclic/ZModulo/ZModulo.v
@@ -466,8 +466,8 @@ Section ZModulo.
  generalize (Zgcd_is_gcd a b); inversion_clear 1.
  destruct H2 as (q,H2); destruct H3 as (q',H3); clear H4.
  assert (H4:=Z.gcd_nonneg a b).
- destruct (Z.eq_dec (Z.gcd a b) 0).
- rewrite e; generalize (Zmax_spec a b); omega.
+ destruct (Z.eq_dec (Z.gcd a b) 0) as [->|Hneq].
+ generalize (Zmax_spec a b); omega.
  assert (0 <= q).
   apply Z.mul_le_mono_pos_r with (Z.gcd a b); auto with zarith.
  destruct (Z.eq_dec q 0).
-- 
cgit v1.2.3