diff options
Diffstat (limited to 'theories/Numbers/Integer/BigZ/ZMake.v')
| -rw-r--r-- | theories/Numbers/Integer/BigZ/ZMake.v | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/theories/Numbers/Integer/BigZ/ZMake.v b/theories/Numbers/Integer/BigZ/ZMake.v index f4baf32bc..4c4eb6c10 100644 --- a/theories/Numbers/Integer/BigZ/ZMake.v +++ b/theories/Numbers/Integer/BigZ/ZMake.v @@ -461,7 +461,7 @@ Module Make (N:NType) <: ZType. | Neg nx, Neg ny => Pos (N.div nx ny) end. - Definition remainder x y := + Definition rem x y := if eq_bool y zero then x else match x, y with @@ -478,10 +478,10 @@ Module Make (N:NType) <: ZType. rewrite Zquot_Zdiv_pos; trivial using N.spec_pos. Qed. - Lemma spec_remainder : forall x y, - to_Z (remainder x y) = (to_Z x) rem (to_Z y). + Lemma spec_rem : forall x y, + to_Z (rem x y) = Zrem (to_Z x) (to_Z y). Proof. - intros x y. unfold remainder. rewrite spec_eq_bool, spec_0. + intros x y. unfold rem. rewrite spec_eq_bool, spec_0. assert (Hy := Zeq_bool_if (to_Z y) 0). destruct Zeq_bool. now rewrite Hy, Zrem_0_r. destruct x as [x|x], y as [y|y]; simpl in *; symmetry; |