From 8be036afb4445cdc009bfb244fbf593dacbe95b7 Mon Sep 17 00:00:00 2001 From: Kazuhiko Sakaguchi Date: Thu, 29 Oct 2020 12:29:08 +0900 Subject: Add `dvdpNl` and rename `dvdpN` to `dvdpNr` Co-authored-by: Cyril Cohen --- mathcomp/algebra/polydiv.v | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) (limited to 'mathcomp/algebra') diff --git a/mathcomp/algebra/polydiv.v b/mathcomp/algebra/polydiv.v index ebb8a5b..356b8ae 100644 --- a/mathcomp/algebra/polydiv.v +++ b/mathcomp/algebra/polydiv.v @@ -1434,7 +1434,12 @@ Proof. by move=> cn0; exact/eqp_dvdr/eqp_scale. Qed. Lemma dvdpZl c m n : c != 0 -> (c *: m %| n) = (m %| n). Proof. by move=> cn0; exact/eqp_dvdl/eqp_scale. Qed. -Lemma dvdpN d p : d %| (- p) = (d %| p). +Lemma dvdpNl d p : (- d) %| p = (d %| p). +Proof. +by rewrite -scaleN1r; apply/eqp_dvdl/eqp_scale; rewrite oppr_eq0 oner_neq0. +Qed. + +Lemma dvdpNr d p : d %| (- p) = (d %| p). Proof. by apply: eqp_dvdr; rewrite -scaleN1r eqp_scale ?oppr_eq0 ?oner_eq0. Qed. Lemma eqp_mul2r r p q : r != 0 -> (p * r %= q * r) = (p %= q). @@ -2358,7 +2363,7 @@ Notation "@ 'dvdp_scalel'" := Notation "@ 'dvdp_scaler'" := (deprecate dvdp_scaler dvdpZr) (at level 10, only parsing) : fun_scope. Notation "@ 'dvdp_opp'" := - (deprecate dvdp_opp dvdpN) (at level 10, only parsing) : fun_scope. + (deprecate dvdp_opp dvdpNr) (at level 10, only parsing) : fun_scope. Notation "@ 'coprimep_scalel'" := (deprecate coprimep_scalel coprimepZl) (at level 10, only parsing) : fun_scope. Notation "@ 'coprimep_scaler'" := -- cgit v1.2.3