(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.                  *)
(* Distributed under the terms of CeCILL-B.                                  *)
Require Import mathcomp.ssreflect.ssreflect.
From mathcomp
Require Import ssrbool ssrfun eqtype ssrnat seq path div choice.
From mathcomp
Require Import fintype tuple finfun bigop prime ssralg poly ssrnum ssrint rat.
From mathcomp
Require Import polydiv finalg perm zmodp matrix mxalgebra vector.

(******************************************************************************)
(* This file provides various results on divisibility of integers.            *)
(* It defines, for m, n, d : int,                                             *)
(*   (m %% d)%Z == the remainder of the Euclidean division of m by d; this is *)
(*                 the least non-negative element of the coset m + dZ when    *)
(*                 d != 0, and m if d = 0.                                    *)
(*   (m %/ d)%Z == the quotient of the Euclidean division of m by d, such     *)
(*                 that m = (m %/ d)%Z * d + (m %% d)%Z. Since for d != 0 the *)
(*                 remainder is non-negative, (m %/ d)%Z is non-zero for      *)
(*   (d %| m)%Z <=> m is divisible by d; dvdz d is the (collective) predicate *)
(*                 for integers divisible by d, and (d %| m)%Z is actually    *)
(*                 (transposing) notation for m \in dvdz d.                   *)
(* (m = n %[mod d])%Z, (m == n %[mod d])%Z, (m != n %[mod d])%Z               *)
(*                 m and n are (resp. compare, don't compare) equal mod d.    *)
(*     gcdz m n == the (non-negative) greatest common divisor of m and n,     *)
(*                 with gcdz 0 0 = 0.                                         *)
(* coprimez m n <=> m and n are coprime.                                      *)
(*    egcdz m n == the Bezout coefficients of the gcd of m and n: a pair      *)
(*                 (u, v) of coprime integers such that u*m + v*n = gcdz m n. *)
(*                 Alternatively, a Bezoutz lemma states such u and v exist.  *)
(* zchinese m1 m2 n1 n2 == for coprime m1 and m2, a solution to the Chinese   *)
(*                 remainder problem for n1 and n2, i.e., and integer n such  *)
(*                 that n = n1 %[mod m1] and n = n2 %[mod m2].                *)
(*  zcontents p == the contents of p : {poly int}, that is, the gcd of the    *)
(*                 coefficients of p, with the lead coefficient of p,         *)
(* zprimitive p == the primitive part of p : {poly int}, i.e., p divided by   *)
(*                 its contents.                                              *)
(* inIntSpan X v <-> v is an integral linear combination of elements of       *)
(*                 X : seq V, where V is a zmodType. We prove that this is a  *)
(*                 decidable property for Q-vector spaces.                    *)
(* int_Smith_normal_form :: a theorem asserting the existence of the Smith    *)
(*                 normal form for integer matrices.                          *)
(* Note that many of the concepts and results in this file could and perhaps  *)
(* sould be generalized to the more general setting of integral, unique       *)
(* factorization, principal ideal, or Euclidean domains.                      *)
(******************************************************************************)

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Import GRing.Theory Num.Theory.
Local Open Scope ring_scope.

Definition divz (m d : int) :=
  let: (K, n) := match m with Posz n => (Posz, n) | Negz n => (Negz, n) end in
  sgz d * K (n %/ `|d|)%N.

Definition modz (m d : int) : int := m - divz m d * d.

Definition dvdz d m := (`|d| %| `|m|)%N.

Definition gcdz m n := (gcdn `|m| `|n|)%:Z.

Definition egcdz m n : int * int :=
  if m == 0 then (0, (-1) ^+ (n < 0)%R) else
  let: (u, v) := egcdn `|m| `|n| in (sgz m * u, - (-1) ^+ (n < 0)%R * v%:Z).

Definition coprimez m n := (gcdz m n == 1).

Infix "%/" := divz : int_scope.
Infix "%%" := modz : int_scope.
Notation "d %| m" := (m \in dvdz d) : int_scope.
Notation "m = n %[mod d ]" := (modz m d = modz n d) : int_scope.
Notation "m == n %[mod d ]" := (modz m d == modz n d) : int_scope.
Notation "m <> n %[mod d ]" := (modz m d <> modz n d) : int_scope.
Notation "m != n %[mod d ]" := (modz m d != modz n d) : int_scope.

Lemma divz_nat (n d : nat) : (n %/ d)%Z = (n %/ d)%N.
Proof. by case: d => // d; rewrite /divz /= mul1r. Qed.

Lemma divzN m d : (m %/ - d)%Z = - (m %/ d)%Z.
Proof. by case: m => n; rewrite /divz /= sgzN abszN mulNr. Qed.

Lemma divz_abs m d : (m %/ `|d|)%Z = (-1) ^+ (d < 0)%R * (m %/ d)%Z.
Proof.
by rewrite {3}[d]intEsign !mulr_sign; case: ifP => -> //; rewrite divzN opprK.
Qed.

Lemma div0z d : (0 %/ d)%Z = 0.
Proof.
by rewrite -(canLR (signrMK _) (divz_abs _ _)) (divz_nat 0) div0n mulr0.
Qed.

Lemma divNz_nat m d : (d > 0)%N -> (Negz m %/ d)%Z = - (m %/ d).+1%:Z.
Proof. by case: d => // d _; apply: mul1r. Qed.

Lemma divz_eq m d : m = (m %/ d)%Z * d + (m %% d)%Z.
Proof. by rewrite addrC subrK. Qed.

Lemma modzN m d : (m %% - d)%Z = (m %% d)%Z.
Proof. by rewrite /modz divzN mulrNN. Qed.

Lemma modz_abs m d : (m %% `|d|%N)%Z = (m %% d)%Z.
Proof. by rewrite {2}[d]intEsign mulr_sign; case: ifP; rewrite ?modzN. Qed.

Lemma modz_nat (m d : nat) : (m %% d)%Z = (m %% d)%N.
Proof.
by apply: (canLR (addrK _)); rewrite addrC divz_nat {1}(divn_eq m d).
Qed.

Lemma modNz_nat m d : (d > 0)%N -> (Negz m %% d)%Z = d%:Z - 1 - (m %% d)%:Z.
Proof.
rewrite /modz => /divNz_nat->; apply: (canLR (addrK _)).
rewrite -!addrA -!opprD -!PoszD -opprB mulnSr !addnA PoszD addrK.
by rewrite addnAC -addnA mulnC -divn_eq.
Qed.

Lemma modz_ge0 m d : d != 0 -> 0 <= (m %% d)%Z.
Proof.
rewrite -absz_gt0 -modz_abs => d_gt0.
case: m => n; rewrite ?modNz_nat ?modz_nat // -addrA -opprD subr_ge0.
by rewrite lez_nat ltn_mod.
Qed.

Lemma divz0 m : (m %/ 0)%Z = 0. Proof. by case: m. Qed.
Lemma mod0z d : (0 %% d)%Z = 0. Proof. by rewrite /modz div0z mul0r subrr. Qed.
Lemma modz0 m : (m %% 0)%Z = m. Proof. by rewrite /modz mulr0 subr0. Qed.

Lemma divz_small m d : 0 <= m < `|d|%:Z -> (m %/ d)%Z = 0.
Proof.
rewrite -(canLR (signrMK _) (divz_abs _ _)); case: m => // n /divn_small.
by rewrite divz_nat => ->; rewrite mulr0.
Qed.

Lemma divzMDl q m d : d != 0 -> ((q * d + m) %/ d)%Z = q + (m %/ d)%Z.
Proof.
rewrite neqr_lt -oppr_gt0 => nz_d.
wlog{nz_d} d_gt0: q d / d > 0; last case: d => // d in d_gt0 *.
  move=> IH; case/orP: nz_d => /IH// /(_  (- q)).
  by rewrite mulrNN !divzN -opprD => /oppr_inj.
wlog q_gt0: q m / q >= 0; last case: q q_gt0 => // q _.
  move=> IH; case: q => n; first exact: IH; rewrite NegzE mulNr.
  by apply: canRL (addKr _) _; rewrite -IH ?addNKr.
case: m => n; first by rewrite !divz_nat divnMDl.
have [le_qd_n | lt_qd_n] := leqP (q * d) n.
  rewrite divNz_nat // NegzE -(subnKC le_qd_n) divnMDl //.
  by rewrite -!addnS !PoszD !opprD !addNKr divNz_nat.
rewrite divNz_nat // NegzE -PoszM subzn // divz_nat.
apply: canRL (addrK _) _; congr _%:Z; rewrite addnC -divnMDl // mulSnr.
rewrite -{3}(subnKC (ltn_pmod n d_gt0)) addnA addnS -divn_eq addnAC.
by rewrite subnKC // divnMDl // divn_small ?addn0 // subnSK ?ltn_mod ?leq_subr.
Qed.

Lemma mulzK m d : d != 0 -> (m * d %/ d)%Z = m.
Proof. by move=> d_nz; rewrite -[m * d]addr0 divzMDl // div0z addr0. Qed.

Lemma mulKz m d : d != 0 -> (d * m %/ d)%Z = m.
Proof. by move=> d_nz; rewrite mulrC mulzK. Qed.

Lemma expzB p m n : p != 0 -> (m >= n)%N -> p ^+ (m - n) = (p ^+ m %/ p ^+ n)%Z.
Proof. by move=> p_nz /subnK{2}<-; rewrite exprD mulzK // expf_neq0. Qed.

Lemma modz1 m : (m %% 1)%Z = 0.
Proof. by case: m => n; rewrite (modNz_nat, modz_nat) ?modn1. Qed.

Lemma divz1 m : (m %/ 1)%Z = m. Proof. by rewrite -{1}[m]mulr1 mulzK. Qed.

Lemma divzz d : (d %/ d)%Z = (d != 0).
Proof. by have [-> // | d_nz] := altP eqP; rewrite -{1}[d]mul1r mulzK. Qed.

Lemma ltz_pmod m d : d > 0 -> (m %% d)%Z < d.
Proof.
case: m d => n [] // d d_gt0; first by rewrite modz_nat ltz_nat ltn_pmod.
by rewrite modNz_nat // -lez_addr1 addrAC subrK ger_addl oppr_le0.
Qed.

Lemma ltz_mod m d : d != 0 -> (m %% d)%Z < `|d|.
Proof. by rewrite -absz_gt0 -modz_abs => d_gt0; apply: ltz_pmod. Qed.

Lemma divzMpl p m d : p > 0 -> (p * m %/ (p * d) = m %/ d)%Z.
Proof.
case: p => // p p_gt0; wlog d_gt0: d / d > 0; last case: d => // d in d_gt0 *.
  by move=> IH; case/intP: d => [|d|d]; rewrite ?mulr0 ?divz0 ?mulrN ?divzN ?IH.
rewrite {1}(divz_eq m d) mulrDr mulrCA divzMDl ?mulf_neq0 ?gtr_eqF // addrC.
rewrite divz_small ?add0r // PoszM pmulr_rge0 ?modz_ge0 ?gtr_eqF //=.
by rewrite ltr_pmul2l ?ltz_pmod.
Qed.
Arguments divzMpl [p m d].

Lemma divzMpr p m d : p > 0 -> (m * p %/ (d * p) = m %/ d)%Z.
Proof. by move=> p_gt0; rewrite -!(mulrC p) divzMpl. Qed.
Arguments divzMpr [p m d].

Lemma lez_floor m d : d != 0 -> (m %/ d)%Z * d <= m.
Proof. by rewrite -subr_ge0; apply: modz_ge0. Qed.

(* leq_mod does not extend to negative m. *)
Lemma lez_div m d : (`|(m %/ d)%Z| <= `|m|)%N.
Proof.
wlog d_gt0: d / d > 0; last case: d d_gt0 => // d d_gt0.
  by move=> IH; case/intP: d => [|n|n]; rewrite ?divz0 ?divzN ?abszN // IH.
case: m => n; first by rewrite divz_nat leq_div.
by rewrite divNz_nat // NegzE !abszN ltnS leq_div.
Qed.
 
Lemma ltz_ceil m d : d > 0 -> m < ((m %/ d)%Z + 1) * d.
Proof.
by case: d => // d d_gt0; rewrite mulrDl mul1r -ltr_subl_addl ltz_mod ?gtr_eqF.
Qed.

Lemma ltz_divLR m n d : d > 0 -> ((m %/ d)%Z < n) = (m < n * d).
Proof.
move=> d_gt0; apply/idP/idP.
  by rewrite -lez_addr1 -(ler_pmul2r d_gt0); apply: ltr_le_trans (ltz_ceil _ _).
rewrite -(ltr_pmul2r d_gt0 _ n) //; apply: ler_lt_trans (lez_floor _ _).
by rewrite gtr_eqF.
Qed.

Lemma lez_divRL m n d : d > 0 -> (m <= (n %/ d)%Z) = (m * d <= n).
Proof. by move=> d_gt0; rewrite !lerNgt ltz_divLR. Qed.

Lemma divz_ge0 m d : d > 0 -> ((m %/ d)%Z >= 0) = (m >= 0).
Proof. by case: d m => // d [] n d_gt0; rewrite (divz_nat, divNz_nat). Qed.

Lemma divzMA_ge0 m n p : n >= 0 -> (m %/ (n * p) = (m %/ n)%Z %/ p)%Z.
Proof.
case: n => // [[|n]] _; first by rewrite mul0r !divz0 div0z.
wlog p_gt0: p / p > 0; last case: p => // p in p_gt0 *.
  by case/intP: p => [|p|p] IH; rewrite ?mulr0 ?divz0 ?mulrN ?divzN // IH.
rewrite {2}(divz_eq m (n.+1%:Z * p)) mulrA mulrAC !divzMDl // ?gtr_eqF //.
rewrite [rhs in _ + rhs]divz_small ?addr0 // ltz_divLR // divz_ge0 //.
by rewrite mulrC ltz_pmod ?modz_ge0 ?gtr_eqF ?pmulr_lgt0.
Qed.

Lemma modz_small m d : 0 <= m < d -> (m %% d)%Z = m.
Proof. by case: m d => //= m [] // d; rewrite modz_nat => /modn_small->. Qed.

Lemma modz_mod m d : ((m %% d)%Z = m %[mod d])%Z.
Proof.
rewrite -!(modz_abs _ d); case: {d}`|d|%N => [|d]; first by rewrite !modz0.
by rewrite modz_small ?modz_ge0 ?ltz_mod.
Qed.

Lemma modzMDl p m d : (p * d + m = m %[mod d])%Z.
Proof.
have [-> | d_nz] := eqVneq d 0; first by rewrite mulr0 add0r.
by rewrite /modz divzMDl // mulrDl opprD addrACA subrr add0r.
Qed.

Lemma mulz_modr {p m d} : 0 < p -> p * (m %% d)%Z = ((p * m) %% (p * d))%Z.
Proof.
case: p => // p p_gt0; rewrite mulrBr; apply: canLR (addrK _) _.
by rewrite mulrCA -(divzMpl p_gt0) subrK.
Qed.

Lemma mulz_modl {p m d} : 0 < p -> (m %% d)%Z * p = ((m * p) %% (d * p))%Z.
Proof. by rewrite -!(mulrC p); apply: mulz_modr. Qed.

Lemma modzDl m d : (d + m = m %[mod d])%Z.
Proof. by rewrite -{1}[d]mul1r modzMDl. Qed.

Lemma modzDr m d : (m + d = m %[mod d])%Z.
Proof. by rewrite addrC modzDl. Qed.

Lemma modzz d : (d %% d)%Z = 0.
Proof. by rewrite -{1}[d]addr0 modzDl mod0z. Qed.

Lemma modzMl p d : (p * d %% d)%Z = 0.
Proof. by rewrite -[p * d]addr0 modzMDl mod0z. Qed.

Lemma modzMr p d : (d * p %% d)%Z = 0.
Proof. by rewrite mulrC modzMl. Qed.

Lemma modzDml m n d : ((m %% d)%Z + n = m + n %[mod d])%Z.
Proof. by rewrite {2}(divz_eq m d) -[_ * d + _ + n]addrA modzMDl. Qed.

Lemma modzDmr m n d : (m + (n %% d)%Z = m + n %[mod d])%Z.
Proof. by rewrite !(addrC m) modzDml. Qed.

Lemma modzDm m n d : ((m %% d)%Z + (n %% d)%Z = m + n %[mod d])%Z.
Proof. by rewrite modzDml modzDmr. Qed.

Lemma eqz_modDl p m n d : (p + m == p + n %[mod d])%Z = (m == n %[mod d])%Z.
Proof.
have [-> | d_nz] := eqVneq d 0; first by rewrite !modz0 (inj_eq (addrI p)).
apply/eqP/eqP=> eq_mn; last by rewrite -modzDmr eq_mn modzDmr.
by rewrite -(addKr p m) -modzDmr eq_mn modzDmr addKr.
Qed.

Lemma eqz_modDr p m n d : (m + p == n + p %[mod d])%Z = (m == n %[mod d])%Z.
Proof. by rewrite -!(addrC p) eqz_modDl. Qed.

Lemma modzMml m n d : ((m %% d)%Z * n = m * n %[mod d])%Z.
Proof. by rewrite {2}(divz_eq m d) mulrDl mulrAC modzMDl. Qed.

Lemma modzMmr m n d : (m * (n %% d)%Z = m * n %[mod d])%Z.
Proof. by rewrite !(mulrC m) modzMml. Qed.

Lemma modzMm m n d : ((m %% d)%Z * (n %% d)%Z = m * n %[mod d])%Z.
Proof. by rewrite modzMml modzMmr. Qed.

Lemma modzXm k m d : ((m %% d)%Z ^+ k = m ^+ k %[mod d])%Z.
Proof. by elim: k => // k IHk; rewrite !exprS -modzMmr IHk modzMm. Qed.

Lemma modzNm m d : (- (m %% d)%Z = - m %[mod d])%Z.
Proof. by rewrite -mulN1r modzMmr mulN1r. Qed.

Lemma modz_absm m d : ((-1) ^+ (m < 0)%R * (m %% d)%Z = `|m|%:Z %[mod d])%Z.
Proof. by rewrite modzMmr -abszEsign. Qed.

(** Divisibility **)

Fact dvdz_key d : pred_key (dvdz d). Proof. by []. Qed.
Canonical dvdz_keyed d := KeyedPred (dvdz_key d).

Lemma dvdzE d m : (d %| m)%Z = (`|d| %| `|m|)%N. Proof. by []. Qed.
Lemma dvdz0 d : (d %| 0)%Z. Proof. exact: dvdn0. Qed.
Lemma dvd0z n : (0 %| n)%Z = (n == 0). Proof. by rewrite -absz_eq0 -dvd0n. Qed.
Lemma dvdz1 d : (d %| 1)%Z = (`|d|%N == 1%N). Proof. exact: dvdn1. Qed.
Lemma dvd1z m : (1 %| m)%Z. Proof. exact: dvd1n. Qed.
Lemma dvdzz m : (m %| m)%Z. Proof. exact: dvdnn. Qed.

Lemma dvdz_mull d m n : (d %| n)%Z -> (d %| m * n)%Z.
Proof. by rewrite !dvdzE abszM; apply: dvdn_mull. Qed.

Lemma dvdz_mulr d m n : (d %| m)%Z -> (d %| m * n)%Z.
Proof. by move=> d_m; rewrite mulrC dvdz_mull. Qed.
Hint Resolve dvdz0 dvd1z dvdzz dvdz_mull dvdz_mulr : core.

Lemma dvdz_mul d1 d2 m1 m2 : (d1 %| m1 -> d2 %| m2 -> d1 * d2 %| m1 * m2)%Z.
Proof. by rewrite !dvdzE !abszM; apply: dvdn_mul. Qed.

Lemma dvdz_trans n d m : (d %| n -> n %| m -> d %| m)%Z.
Proof. by rewrite !dvdzE; apply: dvdn_trans. Qed.

Lemma dvdzP d m : reflect (exists q, m = q * d) (d %| m)%Z.
Proof.
apply: (iffP dvdnP) => [] [q Dm]; last by exists `|q|%N; rewrite Dm abszM.
exists ((-1) ^+ (m < 0)%R * q%:Z * (-1) ^+ (d < 0)%R).
by rewrite -!mulrA -abszEsign -PoszM -Dm -intEsign.
Qed.
Arguments dvdzP {d m}.

Lemma dvdz_mod0P d m : reflect (m %% d = 0)%Z (d %| m)%Z.
Proof.
apply: (iffP dvdzP) => [[q ->] | md0]; first by rewrite modzMl.
by rewrite (divz_eq m d) md0 addr0; exists (m %/ d)%Z.
Qed.
Arguments dvdz_mod0P {d m}.

Lemma dvdz_eq d m : (d %| m)%Z = ((m %/ d)%Z * d == m).
Proof. by rewrite (sameP dvdz_mod0P eqP) subr_eq0 eq_sym. Qed.

Lemma divzK d m : (d %| m)%Z -> (m %/ d)%Z * d = m.
Proof. by rewrite dvdz_eq => /eqP. Qed.

Lemma lez_divLR d m n : 0 < d -> (d %| m)%Z -> ((m %/ d)%Z <= n) = (m <= n * d).
Proof. by move=> /ler_pmul2r <- /divzK->. Qed.

Lemma ltz_divRL d m n : 0 < d -> (d %| m)%Z -> (n < m %/ d)%Z = (n * d < m).
Proof. by move=> /ltr_pmul2r <- /divzK->. Qed.

Lemma eqz_div d m n : d != 0 -> (d %| m)%Z -> (n == m %/ d)%Z = (n * d == m).
Proof. by move=> /mulIf/inj_eq <- /divzK->. Qed.

Lemma eqz_mul d m n : d != 0 -> (d %| m)%Z -> (m == n * d) = (m %/ d == n)%Z.
Proof. by move=> d_gt0 dv_d_m; rewrite eq_sym -eqz_div // eq_sym. Qed.

Lemma divz_mulAC d m n : (d %| m)%Z -> (m %/ d)%Z * n = (m * n %/ d)%Z.
Proof.
have [-> | d_nz] := eqVneq d 0; first by rewrite !divz0 mul0r.
by move/divzK=> {2} <-; rewrite mulrAC mulzK.
Qed.

Lemma mulz_divA d m n : (d %| n)%Z -> m * (n %/ d)%Z = (m * n %/ d)%Z.
Proof. by move=> dv_d_m; rewrite !(mulrC m) divz_mulAC. Qed.

Lemma mulz_divCA d m n :
  (d %| m)%Z -> (d %| n)%Z -> m * (n %/ d)%Z = n * (m %/ d)%Z.
Proof. by move=> dv_d_m dv_d_n; rewrite mulrC divz_mulAC ?mulz_divA. Qed.

Lemma divzA m n p : (p %| n -> n %| m * p -> m %/ (n %/ p)%Z = m * p %/ n)%Z.
Proof.
move/divzK=> p_dv_n; have [->|] := eqVneq n 0; first by rewrite div0z !divz0.
rewrite -{1 2}p_dv_n mulf_eq0 => /norP[pn_nz p_nz] /divzK; rewrite mulrA p_dv_n.
by move/mulIf=> {1} <- //; rewrite mulzK.
Qed.

Lemma divzMA m n p : (n * p %| m -> m %/ (n * p) = (m %/ n)%Z %/ p)%Z.
Proof.
have [-> | nz_p] := eqVneq p 0; first by rewrite mulr0 !divz0.
have [-> | nz_n] := eqVneq n 0; first by rewrite mul0r !divz0 div0z.
by move/divzK=> {2} <-; rewrite mulrA mulrAC !mulzK.
Qed.

Lemma divzAC m n p : (n * p %| m -> (m %/ n)%Z %/ p =  (m %/ p)%Z %/ n)%Z.
Proof. by move=> np_dv_mn; rewrite -!divzMA // mulrC. Qed.

Lemma divzMl p m d : p != 0 -> (d %| m -> p * m %/ (p * d) = m %/ d)%Z.
Proof.
have [-> | nz_d nz_p] := eqVneq d 0; first by rewrite mulr0 !divz0.
by move/divzK=> {1}<-; rewrite mulrCA mulzK ?mulf_neq0.
Qed.

Lemma divzMr p m d : p != 0 -> (d %| m -> m * p %/ (d * p) = m %/ d)%Z.
Proof. by rewrite -!(mulrC p); apply: divzMl. Qed.

Lemma dvdz_mul2l p d m : p != 0 -> (p * d %| p * m)%Z = (d %| m)%Z.
Proof. by rewrite !dvdzE -absz_gt0 !abszM; apply: dvdn_pmul2l. Qed.
Arguments dvdz_mul2l [p d m].

Lemma dvdz_mul2r p d m : p != 0 -> (d * p %| m * p)%Z = (d %| m)%Z.
Proof. by rewrite !dvdzE -absz_gt0 !abszM; apply: dvdn_pmul2r. Qed.
Arguments dvdz_mul2r [p d m].

Lemma dvdz_exp2l p m n : (m <= n)%N -> (p ^+ m %| p ^+ n)%Z.
Proof. by rewrite dvdzE !abszX; apply: dvdn_exp2l. Qed.

Lemma dvdz_Pexp2l p m n : `|p| > 1 -> (p ^+ m %| p ^+ n)%Z = (m <= n)%N.
Proof. by rewrite dvdzE !abszX ltz_nat; apply: dvdn_Pexp2l. Qed.

Lemma dvdz_exp2r m n k : (m %| n -> m ^+ k %| n ^+ k)%Z.
Proof. by rewrite !dvdzE !abszX; apply: dvdn_exp2r. Qed.

Fact dvdz_zmod_closed d : zmod_closed (dvdz d).
Proof.
split=> [|_ _ /dvdzP[p ->] /dvdzP[q ->]]; first exact: dvdz0.
by rewrite -mulrBl dvdz_mull.
Qed.
Canonical dvdz_addPred d := AddrPred (dvdz_zmod_closed d).
Canonical dvdz_oppPred d := OpprPred (dvdz_zmod_closed d).
Canonical dvdz_zmodPred d := ZmodPred (dvdz_zmod_closed d).
  
Lemma dvdz_exp k d m : (0 < k)%N -> (d %| m -> d %| m ^+ k)%Z.
Proof. by case: k => // k _ d_dv_m; rewrite exprS dvdz_mulr. Qed.

Lemma eqz_mod_dvd d m n : (m == n %[mod d])%Z = (d %| m - n)%Z.
Proof.
apply/eqP/dvdz_mod0P=> eq_mn.
  by rewrite -modzDml eq_mn modzDml subrr mod0z.
by rewrite -(subrK n m) -modzDml eq_mn add0r.
Qed.

Lemma divzDl m n d :
  (d %| m)%Z -> ((m + n) %/ d)%Z = (m %/ d)%Z + (n %/ d)%Z.
Proof.
have [-> | d_nz] := eqVneq d 0; first by rewrite !divz0.
by move/divzK=> {1}<-; rewrite divzMDl.
Qed.

Lemma divzDr m n d :
  (d %| n)%Z -> ((m + n) %/ d)%Z = (m %/ d)%Z + (n %/ d)%Z.
Proof. by move=> dv_n; rewrite addrC divzDl // addrC. Qed.

Lemma Qint_dvdz (m d : int) : (d %| m)%Z -> ((m%:~R / d%:~R : rat) \is a Qint).
Proof.
case/dvdzP=> z ->; rewrite rmorphM /=; case: (altP (d =P 0)) => [->|dn0].
  by rewrite mulr0 mul0r.
by rewrite mulfK ?intr_eq0 // rpred_int.
Qed.

Lemma Qnat_dvd (m d : nat) : (d %| m)%N -> ((m%:R / d%:R : rat) \is a Qnat).
Proof.
move=> h; rewrite Qnat_def divr_ge0 ?ler0n // -[m%:R]/(m%:~R) -[d%:R]/(d%:~R).
by rewrite Qint_dvdz.
Qed.

(* Greatest common divisor *)

Lemma gcdzz m : gcdz m m = `|m|%:Z. Proof. by rewrite /gcdz gcdnn. Qed.
Lemma gcdzC : commutative gcdz. Proof. by move=> m n; rewrite /gcdz gcdnC. Qed.
Lemma gcd0z m : gcdz 0 m = `|m|%:Z. Proof. by rewrite /gcdz gcd0n. Qed.
Lemma gcdz0 m : gcdz m 0 = `|m|%:Z. Proof. by rewrite /gcdz gcdn0. Qed.
Lemma gcd1z : left_zero 1 gcdz. Proof. by move=> m; rewrite /gcdz gcd1n. Qed.
Lemma gcdz1 : right_zero 1 gcdz. Proof. by move=> m; rewrite /gcdz gcdn1. Qed.
Lemma dvdz_gcdr m n : (gcdz m n %| n)%Z. Proof. exact: dvdn_gcdr. Qed.
Lemma dvdz_gcdl m n : (gcdz m n %| m)%Z. Proof. exact: dvdn_gcdl. Qed.
Lemma gcdz_eq0 m n : (gcdz m n == 0) = (m == 0) && (n == 0).
Proof. by rewrite -absz_eq0 eqn0Ngt gcdn_gt0 !negb_or -!eqn0Ngt !absz_eq0. Qed.
Lemma gcdNz m n : gcdz (- m) n = gcdz m n. Proof. by rewrite /gcdz abszN. Qed.
Lemma gcdzN m n : gcdz m (- n) = gcdz m n. Proof. by rewrite /gcdz abszN. Qed.

Lemma gcdz_modr m n : gcdz m (n %% m)%Z = gcdz m n.
Proof.
rewrite -modz_abs /gcdz; move/absz: m => m.
have [-> | m_gt0] := posnP m; first by rewrite modz0.
case: n => n; first by rewrite modz_nat gcdn_modr.
rewrite modNz_nat // NegzE abszN {2}(divn_eq n m) -addnS gcdnMDl.
rewrite -addrA -opprD -intS /=; set m1 := _.+1.
have le_m1m: (m1 <= m)%N by apply: ltn_pmod.
by rewrite subzn // !(gcdnC m) -{2 3}(subnK le_m1m) gcdnDl gcdnDr gcdnC.
Qed.

Lemma gcdz_modl m n : gcdz (m %% n)%Z n = gcdz m n.
Proof. by rewrite -!(gcdzC n) gcdz_modr. Qed.

Lemma gcdzMDl q m n : gcdz m (q * m + n) = gcdz m n.
Proof. by rewrite -gcdz_modr modzMDl gcdz_modr. Qed.
 
Lemma gcdzDl m n : gcdz m (m + n) = gcdz m n.
Proof. by rewrite -{2}(mul1r m) gcdzMDl. Qed.

Lemma gcdzDr m n : gcdz m (n + m) = gcdz m n.
Proof. by rewrite addrC gcdzDl. Qed.

Lemma gcdzMl n m : gcdz n (m * n) = `|n|%:Z.
Proof. by rewrite -[m * n]addr0 gcdzMDl gcdz0. Qed.

Lemma gcdzMr n m : gcdz n (n * m) = `|n|%:Z.
Proof. by rewrite mulrC gcdzMl. Qed.

Lemma gcdz_idPl {m n} : reflect (gcdz m n = `|m|%:Z) (m %| n)%Z.
Proof. by apply: (iffP gcdn_idPl) => [<- | []]. Qed.

Lemma gcdz_idPr {m n} : reflect (gcdz m n = `|n|%:Z) (n %| m)%Z.
Proof. by rewrite gcdzC; apply: gcdz_idPl. Qed.

Lemma expz_min e m n : e >= 0 -> e ^+ minn m n = gcdz (e ^+ m) (e ^+ n).
Proof.
by case: e => // e _; rewrite /gcdz !abszX -expn_min -natz -natrX !natz.
Qed.

Lemma dvdz_gcd p m n : (p %| gcdz m n)%Z = (p %| m)%Z && (p %| n)%Z.
Proof. exact: dvdn_gcd. Qed.

Lemma gcdzAC : right_commutative gcdz.
Proof. by move=> m n p; rewrite /gcdz gcdnAC. Qed.

Lemma gcdzA : associative gcdz.
Proof. by move=> m n p; rewrite /gcdz gcdnA. Qed.

Lemma gcdzCA : left_commutative gcdz.
Proof. by move=> m n p; rewrite /gcdz gcdnCA. Qed.

Lemma gcdzACA : interchange gcdz gcdz.
Proof. by move=> m n p q; rewrite /gcdz gcdnACA. Qed.

Lemma mulz_gcdr m n p : `|m|%:Z * gcdz n p = gcdz (m * n) (m * p).
Proof. by rewrite -PoszM muln_gcdr -!abszM. Qed.

Lemma mulz_gcdl m n p : gcdz m n * `|p|%:Z = gcdz (m * p) (n * p).
Proof. by rewrite -PoszM muln_gcdl -!abszM. Qed.

Lemma mulz_divCA_gcd n m : n * (m %/ gcdz n m)%Z  = m * (n %/ gcdz n m)%Z.
Proof. by rewrite mulz_divCA ?dvdz_gcdl ?dvdz_gcdr. Qed.

(* Not including lcm theory, for now. *)

(* Coprime factors *)

Lemma coprimezE m n : coprimez m n = coprime `|m| `|n|. Proof. by []. Qed.

Lemma coprimez_sym : symmetric coprimez.
Proof. by move=> m n; apply: coprime_sym. Qed.

Lemma coprimeNz m n : coprimez (- m) n = coprimez m n.
Proof. by rewrite coprimezE abszN. Qed.

Lemma coprimezN m n : coprimez m (- n) = coprimez m n.
Proof. by rewrite coprimezE abszN. Qed.

Variant egcdz_spec m n : int * int -> Type :=
  EgcdzSpec u v of u * m + v * n = gcdz m n & coprimez u v
     : egcdz_spec m n (u, v).

Lemma egcdzP m n : egcdz_spec m n (egcdz m n).
Proof.
rewrite /egcdz; have [-> | m_nz] := altP eqP.
  by split; [rewrite -abszEsign gcd0z | rewrite coprimezE absz_sign].
have m_gt0 : (`|m| > 0)%N by rewrite absz_gt0.
case: egcdnP (coprime_egcdn `|n| m_gt0) => //= u v Duv _ co_uv; split.
  rewrite !mulNr -!mulrA mulrCA -abszEsg mulrCA -abszEsign.
  by rewrite -!PoszM Duv addnC PoszD addrK.
by rewrite coprimezE abszM absz_sg m_nz mul1n mulNr abszN abszMsign.
Qed.

Lemma Bezoutz m n : {u : int & {v : int | u * m + v * n = gcdz m n}}.
Proof. by exists (egcdz m n).1, (egcdz m n).2; case: egcdzP. Qed.

Lemma coprimezP m n :
  reflect (exists uv, uv.1 * m + uv.2 * n = 1) (coprimez m n).
Proof.
apply: (iffP eqP) => [<-| [[u v] /= Duv]].
  by exists (egcdz m n); case: egcdzP.
congr _%:Z; apply: gcdn_def; rewrite ?dvd1n // => d dv_d_n dv_d_m.
by rewrite -(dvdzE d 1) -Duv [m]intEsg [n]intEsg rpredD ?dvdz_mull.
Qed.

Lemma Gauss_dvdz m n p :
  coprimez m n -> (m * n %| p)%Z = (m %| p)%Z && (n %| p)%Z.
Proof. by move/Gauss_dvd <-; rewrite -abszM. Qed.

Lemma Gauss_dvdzr m n p : coprimez m n -> (m %| n * p)%Z = (m %| p)%Z.
Proof. by rewrite dvdzE abszM => /Gauss_dvdr->. Qed.

Lemma Gauss_dvdzl m n p : coprimez m p -> (m %| n * p)%Z = (m %| n)%Z.
Proof. by rewrite mulrC; apply: Gauss_dvdzr. Qed.

Lemma Gauss_gcdzr p m n : coprimez p m -> gcdz p (m * n) = gcdz p n.
Proof. by rewrite /gcdz abszM => /Gauss_gcdr->. Qed.

Lemma Gauss_gcdzl p m n : coprimez p n -> gcdz p (m * n) = gcdz p m.
Proof. by move=> co_pn; rewrite mulrC Gauss_gcdzr. Qed.

Lemma coprimez_mulr p m n : coprimez p (m * n) = coprimez p m && coprimez p n.
Proof. by rewrite -coprime_mulr -abszM. Qed.

Lemma coprimez_mull p m n : coprimez (m * n) p = coprimez m p && coprimez n p.
Proof. by rewrite -coprime_mull -abszM. Qed.

Lemma coprimez_pexpl k m n : (0 < k)%N -> coprimez (m ^+ k) n = coprimez m n.
Proof. by rewrite /coprimez /gcdz abszX; apply: coprime_pexpl. Qed.

Lemma coprimez_pexpr k m n : (0 < k)%N -> coprimez m (n ^+ k) = coprimez m n.
Proof. by move=> k_gt0; rewrite !(coprimez_sym m) coprimez_pexpl. Qed.

Lemma coprimez_expl k m n : coprimez m n -> coprimez (m ^+ k) n.
Proof. by rewrite /coprimez /gcdz abszX; apply: coprime_expl. Qed.

Lemma coprimez_expr k m n : coprimez m n -> coprimez m (n ^+ k).
Proof. by rewrite !(coprimez_sym m); apply: coprimez_expl. Qed.

Lemma coprimez_dvdl m n p : (m %| n)%N -> coprimez n p -> coprimez m p.
Proof. exact: coprime_dvdl. Qed.

Lemma coprimez_dvdr m n p : (m %| n)%N -> coprimez p n -> coprimez p m.
Proof. exact: coprime_dvdr. Qed.

Lemma dvdz_pexp2r m n k : (k > 0)%N -> (m ^+ k %| n ^+ k)%Z = (m %| n)%Z.
Proof. by rewrite dvdzE !abszX; apply: dvdn_pexp2r. Qed.

Section Chinese.

(***********************************************************************)
(*   The chinese remainder theorem                                     *)
(***********************************************************************)

Variables m1 m2 : int.
Hypothesis co_m12 : coprimez m1 m2.

Lemma zchinese_remainder x y :
  (x == y %[mod m1 * m2])%Z = (x == y %[mod m1])%Z && (x == y %[mod m2])%Z.
Proof. by rewrite !eqz_mod_dvd Gauss_dvdz. Qed.

(***********************************************************************)
(*   A function that solves the chinese remainder problem              *)
(***********************************************************************)

Definition zchinese r1 r2 :=
  r1 * m2 * (egcdz m1 m2).2 + r2 * m1 * (egcdz m1 m2).1.

Lemma zchinese_modl r1 r2 : (zchinese r1 r2 = r1 %[mod m1])%Z.
Proof.
rewrite /zchinese; have [u v /= Duv _] := egcdzP m1 m2.
rewrite -{2}[r1]mulr1 -((gcdz _ _ =P 1) co_m12) -Duv.
by rewrite mulrDr mulrAC addrC (mulrAC r2) !mulrA !modzMDl.
Qed.

Lemma zchinese_modr r1 r2 : (zchinese r1 r2 = r2 %[mod m2])%Z.
Proof.
rewrite /zchinese; have [u v /= Duv _] := egcdzP m1 m2.
rewrite -{2}[r2]mulr1 -((gcdz _ _ =P 1) co_m12) -Duv.
by rewrite mulrAC modzMDl mulrAC addrC mulrDr !mulrA modzMDl.
Qed.

Lemma zchinese_mod x : (x = zchinese (x %% m1)%Z (x %% m2)%Z %[mod m1 * m2])%Z.
Proof.
apply/eqP; rewrite zchinese_remainder //.
by rewrite zchinese_modl zchinese_modr !modz_mod !eqxx.
Qed.

End Chinese.

Section ZpolyScale.

Definition zcontents p :=
  sgz (lead_coef p) * \big[gcdn/0%N]_(i < size p) `|(p`_i)%R|%N.

Lemma sgz_contents p : sgz (zcontents p) = sgz (lead_coef p).
Proof.
rewrite /zcontents mulrC sgzM sgz_id; set d := _%:Z.
have [-> | nz_p] := eqVneq p 0; first by rewrite lead_coef0 mulr0.
rewrite gtr0_sgz ?mul1r // ltz_nat polySpred ?big_ord_recr //= -lead_coefE.
by rewrite gcdn_gt0 orbC absz_gt0 lead_coef_eq0 nz_p.
Qed.

Lemma zcontents_eq0 p : (zcontents p == 0) = (p == 0).
Proof. by rewrite -sgz_eq0 sgz_contents sgz_eq0 lead_coef_eq0. Qed.

Lemma zcontents0 : zcontents 0 = 0.
Proof. by apply/eqP; rewrite zcontents_eq0. Qed.

Lemma zcontentsZ a p : zcontents (a *: p) = a * zcontents p.
Proof.
have [-> | nz_a] := eqVneq a 0; first by rewrite scale0r mul0r zcontents0.
rewrite {2}[a]intEsg mulrCA -mulrA -PoszM big_distrr /= mulrCA mulrA -sgzM.
rewrite -lead_coefZ; congr (_ * _%:Z); rewrite size_scale //.
by apply: eq_bigr => i _; rewrite coefZ abszM.
Qed.

Lemma zcontents_monic p : p \is monic -> zcontents p = 1.
Proof.
move=> mon_p; rewrite /zcontents polySpred ?monic_neq0 //.
by rewrite big_ord_recr /= -lead_coefE (monicP mon_p) gcdn1.
Qed.

Lemma dvdz_contents a p : (a %| zcontents p)%Z = (p \is a polyOver (dvdz a)).
Proof.
rewrite dvdzE abszM absz_sg lead_coef_eq0.
have [-> | nz_p] := altP eqP; first by rewrite mul0n dvdn0 rpred0.
rewrite mul1n; apply/dvdn_biggcdP/(all_nthP 0)=> a_dv_p i ltip /=.
  exact: (a_dv_p (Ordinal ltip)).
exact: a_dv_p.
Qed.

Lemma map_poly_divzK {a} p :
  p \is a polyOver (dvdz a) -> a *: map_poly (divz^~ a) p = p.
Proof.
move/polyOverP=> a_dv_p; apply/polyP=> i.
by rewrite coefZ coef_map_id0 ?div0z // mulrC divzK.
Qed.

Lemma polyOver_dvdzP a p :
  reflect (exists q, p = a *: q) (p \is a polyOver (dvdz a)).
Proof.
apply: (iffP idP) => [/map_poly_divzK | [q ->]].
  by exists (map_poly (divz^~ a) p).
by apply/polyOverP=> i; rewrite coefZ dvdz_mulr.
Qed.

Definition zprimitive p := map_poly (divz^~ (zcontents p)) p.

Lemma zpolyEprim p : p = zcontents p *: zprimitive p.
Proof. by rewrite map_poly_divzK // -dvdz_contents. Qed.

Lemma zprimitive0 : zprimitive 0 = 0.
Proof.
by apply/polyP=> i; rewrite coef0 coef_map_id0 ?div0z // zcontents0 divz0.
Qed.

Lemma zprimitive_eq0 p : (zprimitive p == 0) = (p == 0).
Proof.
apply/idP/idP=> /eqP p0; first by rewrite [p]zpolyEprim p0 scaler0.
by rewrite p0 zprimitive0.
Qed.

Lemma size_zprimitive p : size (zprimitive p) = size p.
Proof.
have [-> | ] := eqVneq p 0; first by rewrite zprimitive0.
by rewrite {1 3}[p]zpolyEprim scale_poly_eq0 => /norP[/size_scale-> _].
Qed.

Lemma sgz_lead_primitive p : sgz (lead_coef (zprimitive p)) = (p != 0).
Proof.
have [-> | nz_p] := altP eqP; first by rewrite zprimitive0 lead_coef0.
apply: (@mulfI _ (sgz (zcontents p))); first by rewrite sgz_eq0 zcontents_eq0.
by rewrite -sgzM mulr1 -lead_coefZ -zpolyEprim sgz_contents.
Qed.

Lemma zcontents_primitive p : zcontents (zprimitive p) = (p != 0).
Proof.
have [-> | nz_p] := altP eqP; first by rewrite zprimitive0 zcontents0.
apply: (@mulfI _ (zcontents p)); first by rewrite zcontents_eq0.
by rewrite mulr1 -zcontentsZ -zpolyEprim.
Qed.

Lemma zprimitive_id p : zprimitive (zprimitive p) = zprimitive p.
Proof.
have [-> | nz_p] := eqVneq p 0; first by rewrite !zprimitive0.
by rewrite {2}[zprimitive p]zpolyEprim zcontents_primitive nz_p scale1r.
Qed.

Lemma zprimitive_monic p : p \in monic -> zprimitive p = p.
Proof. by move=> mon_p; rewrite {2}[p]zpolyEprim zcontents_monic ?scale1r. Qed.

Lemma zprimitiveZ a p : a != 0 -> zprimitive (a *: p) = zprimitive p.
Proof.
have [-> | nz_p nz_a] := eqVneq p 0; first by rewrite scaler0.
apply: (@mulfI _ (a * zcontents p)%:P).
  by rewrite polyC_eq0 mulf_neq0 ?zcontents_eq0.
by rewrite -{1}zcontentsZ !mul_polyC -zpolyEprim -scalerA -zpolyEprim.
Qed.

Lemma zprimitive_min p a q :
    p != 0 -> p = a *: q ->
  {b | sgz b = sgz (lead_coef q) & q = b *: zprimitive p}.
Proof.
move=> nz_p Dp; have /dvdzP/sig_eqW[b Db]: (a %| zcontents p)%Z.
  by rewrite dvdz_contents; apply/polyOver_dvdzP; exists q.
suffices ->: q = b *: zprimitive p.
  by rewrite lead_coefZ sgzM sgz_lead_primitive nz_p mulr1; exists b.
apply: (@mulfI _ a%:P).
  by apply: contraNneq nz_p; rewrite Dp -mul_polyC => ->; rewrite mul0r.
by rewrite !mul_polyC -Dp scalerA mulrC -Db -zpolyEprim.
Qed.

Lemma zprimitive_irr p a q :
  p != 0 -> zprimitive p = a *: q -> a = sgz (lead_coef q).
Proof.
move=> nz_p Dp; have: p = (a * zcontents p) *: q.
  by rewrite mulrC -scalerA -Dp -zpolyEprim.
case/zprimitive_min=> // b <- /eqP.
rewrite Dp -{1}[q]scale1r scalerA -subr_eq0 -scalerBl scale_poly_eq0 subr_eq0.
have{Dp} /negPf->: q != 0.
  by apply: contraNneq nz_p; rewrite -zprimitive_eq0 Dp => ->; rewrite scaler0.
by case: b a => [[|[|b]] | [|b]] [[|[|a]] | [|a]] //; rewrite mulr0.
Qed.

Lemma zcontentsM p q : zcontents (p * q) = zcontents p * zcontents q.
Proof.
have [-> | nz_p] := eqVneq p 0; first by rewrite !(mul0r, zcontents0).
have [-> | nz_q] := eqVneq q 0; first by rewrite !(mulr0, zcontents0).
rewrite -[zcontents q]mulr1 {1}[p]zpolyEprim {1}[q]zpolyEprim.
rewrite -scalerAl -scalerAr !zcontentsZ; congr (_ * (_ * _)).
rewrite [zcontents _]intEsg sgz_contents lead_coefM sgzM !sgz_lead_primitive.
apply/eqP; rewrite nz_p nz_q !mul1r [_ == _]eqn_leq absz_gt0 zcontents_eq0.
rewrite mulf_neq0 ?zprimitive_eq0 // andbT leqNgt.
apply/negP=> /pdivP[r r_pr r_dv_d]; pose to_r : int -> 'F_r := intr.
have nz_prim_r q1: q1 != 0 -> map_poly to_r (zprimitive q1) != 0.
  move=> nz_q1; apply: contraTneq (prime_gt1 r_pr) => r_dv_q1.
  rewrite -leqNgt dvdn_leq // -(dvdzE r true) -nz_q1 -zcontents_primitive.
  rewrite dvdz_contents; apply/polyOverP=> i /=; rewrite dvdzE /=.
  have /polyP/(_ i)/eqP := r_dv_q1; rewrite coef_map coef0 /=.
  rewrite {1}[_`_i]intEsign rmorphM rmorph_sign /= mulf_eq0 signr_eq0 /=.
  by rewrite -val_eqE /= val_Fp_nat.
suffices{nz_prim_r} /idPn[]: map_poly to_r (zprimitive p * zprimitive q) == 0.
  by rewrite rmorphM mulf_neq0 ?nz_prim_r.
rewrite [_ * _]zpolyEprim [zcontents _]intEsign mulrC -scalerA map_polyZ /=.
by rewrite scale_poly_eq0 -val_eqE /= val_Fp_nat ?(eqnP r_dv_d).
Qed.


Lemma zprimitiveM p q : zprimitive (p * q) = zprimitive p * zprimitive q.
Proof.
have [pq_0|] := eqVneq (p * q) 0.
  rewrite pq_0; move/eqP: pq_0; rewrite mulf_eq0.
  by case/pred2P=> ->; rewrite !zprimitive0 (mul0r, mulr0).
rewrite -zcontents_eq0 -polyC_eq0 => /mulfI; apply; rewrite !mul_polyC.
by rewrite -zpolyEprim zcontentsM -scalerA scalerAr scalerAl -!zpolyEprim.
Qed.

Lemma dvdpP_int p q : p %| q -> {r | q = zprimitive p * r}.
Proof.
case/Pdiv.Idomain.dvdpP/sig2_eqW=> [[c r] /= nz_c Dpr].
exists (zcontents q *: zprimitive r); rewrite -scalerAr.
by rewrite -zprimitiveM mulrC -Dpr zprimitiveZ // -zpolyEprim.
Qed.

Local Notation pZtoQ := (map_poly (intr : int -> rat)).

Lemma size_rat_int_poly p : size (pZtoQ p) = size p.
Proof. by apply: size_map_inj_poly; first apply: intr_inj. Qed.

Lemma rat_poly_scale (p : {poly rat}) :
  {q : {poly int} & {a | a != 0 & p = a%:~R^-1 *: pZtoQ q}}.
Proof.
pose a := \prod_(i < size p) denq p`_i.
have nz_a: a != 0 by apply/prodf_neq0=> i _; apply: denq_neq0.
exists (map_poly numq (a%:~R *: p)), a => //.
apply: canRL (scalerK _) _; rewrite ?intr_eq0 //.
apply/polyP=> i; rewrite !(coefZ, coef_map_id0) // numqK // Qint_def mulrC.
have [ltip | /(nth_default 0)->] := ltnP i (size p); last by rewrite mul0r.
by rewrite [a](bigD1 (Ordinal ltip)) // rmorphM mulrA -numqE -rmorphM denq_int.
Qed.

Lemma dvdp_rat_int p q : (pZtoQ p %| pZtoQ q) = (p %| q).
Proof.
apply/dvdpP/Pdiv.Idomain.dvdpP=> [[/= r1 Dq] | [[/= a r] nz_a Dq]]; last first.
  exists (a%:~R^-1 *: pZtoQ r); rewrite -scalerAl -rmorphM -Dq.
  by rewrite -{2}[a]intz scaler_int rmorphMz -scaler_int scalerK ?intr_eq0.
have [r [a nz_a Dr1]] := rat_poly_scale r1; exists (a, r) => //=.
apply: (map_inj_poly _ _ : injective pZtoQ) => //; first exact: intr_inj.
rewrite -[a]intz scaler_int rmorphMz -scaler_int /= Dq Dr1.
by rewrite -scalerAl -rmorphM scalerKV ?intr_eq0.
Qed.

Lemma dvdpP_rat_int p q :
    p %| pZtoQ q ->
  {p1 : {poly int} & {a | a != 0 & p = a *: pZtoQ p1} & {r | q = p1 * r}}.
Proof.
have{p} [p [a nz_a ->]] := rat_poly_scale p.
rewrite dvdp_scalel ?invr_eq0 ?intr_eq0 // dvdp_rat_int => dv_p_q.
exists (zprimitive p); last exact: dvdpP_int.
have [-> | nz_p] := eqVneq p 0.
  by exists 1; rewrite ?oner_eq0 // zprimitive0 map_poly0 !scaler0.
exists ((zcontents p)%:~R / a%:~R).
  by rewrite mulf_neq0 ?invr_eq0 ?intr_eq0 ?zcontents_eq0.
by rewrite mulrC -scalerA -map_polyZ -zpolyEprim.
Qed.

End ZpolyScale.

(* Integral spans. *)

Lemma int_Smith_normal_form m n (M : 'M[int]_(m, n)) :
  {L : 'M[int]_m & L \in unitmx &
  {R : 'M[int]_n & R \in unitmx &
  {d : seq int | sorted dvdz d &
   M = L *m (\matrix_(i, j) (d`_i *+ (i == j :> nat))) *m R}}}.
Proof.
move: {2}_.+1 (ltnSn (m + n)) => mn.
elim: mn => // mn IHmn in m n M *; rewrite ltnS => le_mn.
have [[i j] nzMij | no_ij] := pickP (fun k => M k.1 k.2 != 0%N); last first.
  do 2![exists 1%:M; first exact: unitmx1]; exists nil => //=.
  apply/matrixP=> i j; apply/eqP; rewrite mulmx1 mul1mx mxE nth_nil mul0rn.
  exact: negbFE (no_ij (i, j)).
do [case: m i => [[]//|m] i; case: n j => [[]//|n] j /=] in M nzMij le_mn *.
wlog Dj: j M nzMij / j = 0; last rewrite {j}Dj in nzMij.
  case/(_ 0 (xcol j 0 M)); rewrite ?mxE ?tpermR // => L uL [R uR [d dvD dM]].
  exists L => //; exists (xcol j 0 R); last exists d => //=.
     by rewrite xcolE unitmx_mul uR unitmx_perm.
  by rewrite xcolE !mulmxA -dM xcolE -mulmxA -perm_mxM tperm2 perm_mx1 mulmx1.
move Da: (M i 0) nzMij => a nz_a.
elim: {a}_.+1 {-2}a (ltnSn `|a|) => // A IHa a leA in m n M i Da nz_a le_mn *.
wlog [j a'Mij]: m n M i Da le_mn / {j | ~~ (a %| M i j)%Z}; last first.
  have nz_j: j != 0 by apply: contraNneq a'Mij => ->; rewrite Da.
  case: n => [[[]//]|n] in j le_mn nz_j M a'Mij Da *.
  wlog{nz_j} Dj: j M a'Mij Da / j = 1; last rewrite {j}Dj in a'Mij.
    case/(_ 1 (xcol j 1 M)); rewrite ?mxE ?tpermR ?tpermD //.
    move=> L uL [R uR [d dvD dM]]; exists L => //.
    exists (xcol j 1 R); first by rewrite xcolE unitmx_mul uR unitmx_perm.
    exists d; rewrite //= xcolE !mulmxA -dM xcolE -mulmxA -perm_mxM tperm2.
    by rewrite perm_mx1 mulmx1.
  have [u [v]] := Bezoutz a (M i 1); set b := gcdz _ _ => Db.
  have{leA} ltA: (`|b| < A)%N.
    rewrite -ltnS (leq_trans _ leA) // ltnS ltn_neqAle andbC.
    rewrite dvdn_leq ?absz_gt0 ? dvdn_gcdl //=.
    by rewrite (contraNneq _ a'Mij) ?dvdzE // => <-; apply: dvdn_gcdr.
  pose t2 := [fun j : 'I_2 => [tuple _; _]`_j : int]; pose a1 := M i 1.
  pose Uul := \matrix_(k, j) t2 (t2 u (- (a1 %/ b)%Z) j) (t2 v (a %/ b)%Z j) k.
  pose U : 'M_(2 + n) := block_mx Uul 0 0 1%:M; pose M1 := M *m U.
  have{nz_a} nz_b: b != 0 by rewrite gcdz_eq0 (negPf nz_a).
  have uU: U \in unitmx.
    rewrite unitmxE det_ublock det1 (expand_det_col _ 0) big_ord_recl big_ord1.
    do 2!rewrite /cofactor [row' _ _]mx11_scalar !mxE det_scalar1 /=.
    rewrite mulr1 mul1r mulN1r opprK -[_ + _](mulzK _ nz_b) mulrDl.
    by rewrite -!mulrA !divzK ?dvdz_gcdl ?dvdz_gcdr // Db divzz nz_b unitr1.
  have{Db} Db: M1 i 0 = b.
    rewrite /M1 -(lshift0 n 1) [U]block_mxEh mul_mx_row row_mxEl.
    rewrite -[M](@hsubmxK _ _ 2) (@mul_row_col _ _ 2) mulmx0 addr0 !mxE /=.
    rewrite big_ord_recl big_ord1 !mxE /= [lshift _ _]((_ =P 0) _) // Da.
    by rewrite [lshift _ _]((_ =P 1) _) // mulrC -(mulrC v).
  have [L uL [R uR [d dvD dM1]]] := IHa b ltA _ _ M1 i Db nz_b le_mn.
  exists L => //; exists (R *m invmx U); last exists d => //.
    by rewrite unitmx_mul uR unitmx_inv.
  by rewrite mulmxA -dM1 mulmxK.
move=> {A leA IHa} IHa; wlog Di: i M Da / i = 0; last rewrite {i}Di in Da.
  case/(_ 0 (xrow i 0 M)); rewrite ?mxE ?tpermR // => L uL [R uR [d dvD dM]].
  exists (xrow i 0 L); first by rewrite xrowE unitmx_mul unitmx_perm.
  exists R => //; exists d; rewrite //= xrowE -!mulmxA (mulmxA L) -dM xrowE.
  by rewrite mulmxA -perm_mxM tperm2 perm_mx1 mul1mx.
without loss /forallP a_dvM0: / [forall j, a %| M 0 j]%Z.
  have [_|] := altP forallP; first exact; rewrite negb_forall => /existsP/sigW.
  by move/IHa=> IH _; apply: IH.
without loss{Da a_dvM0} Da: M / forall j, M 0 j = a.
  pose Uur := col' 0 (\row_j (1 - (M 0 j %/ a)%Z)).
  pose U : 'M_(1 + n) := block_mx 1 Uur 0 1%:M; pose M1 := M *m U.
  have uU: U \in unitmx by rewrite unitmxE det_ublock !det1 mulr1.
  case/(_ (M *m U)) => [j | L uL [R uR [d dvD dM]]].
    rewrite -(lshift0 m 0) -[M](@submxK _ 1 _ 1) (@mulmx_block _ 1 m 1).
    rewrite (@col_mxEu _ 1) !mulmx1 mulmx0 addr0 [ulsubmx _]mx11_scalar.
    rewrite mul_scalar_mx !mxE !lshift0 Da.
    case: splitP => [j0 _ | j1 Dj]; rewrite ?ord1 !mxE // lshift0 rshift1.
    by rewrite mulrBr mulr1 mulrC divzK ?subrK.
  exists L => //; exists (R * U^-1); first by rewrite unitmx_mul uR unitmx_inv.
  by exists d; rewrite //= mulmxA -dM mulmxK.
without loss{IHa} /forallP/(_ (_, _))/= a_dvM: / [forall k, a %| M k.1 k.2]%Z.
  have [_|] := altP forallP; first exact; rewrite negb_forall => /existsP/sigW.
  case=> [[i j] /= a'Mij] _.
  have [|||L uL [R uR [d dvD dM]]] := IHa _ _ M^T j; rewrite ?mxE 1?addnC //.
    by exists i; rewrite mxE.
  exists R^T; last exists L^T; rewrite ?unitmx_tr //; exists d => //.
  rewrite -[M]trmxK dM !trmx_mul mulmxA; congr (_ *m _ *m _).
  by apply/matrixP=> i1 j1; rewrite !mxE eq_sym; case: eqP => // ->.
without loss{nz_a a_dvM} a1: M a Da / a = 1.
  pose M1 := map_mx (divz^~ a) M; case/(_ M1 1)=> // [k|L uL [R uR [d dvD dM]]].
    by rewrite !mxE Da divzz nz_a.
  exists L => //; exists R => //; exists [seq a * x | x <- d].
    case: d dvD {dM} => //= x d; elim: d x => //= y d IHd x /andP[dv_xy /IHd].
    by rewrite [dvdz _ _]dvdz_mul2l ?[_ \in _]dv_xy.
  have ->: M = a *: M1 by apply/matrixP=> i j; rewrite !mxE mulrC divzK ?a_dvM.
  rewrite dM scalemxAl scalemxAr; congr (_ *m _ *m _).
  apply/matrixP=> i j; rewrite !mxE mulrnAr; congr (_ *+ _).
  have [lt_i_d | le_d_i] := ltnP i (size d); first by rewrite (nth_map 0).
  by rewrite !nth_default ?size_map ?mulr0.
rewrite {a}a1 -[m.+1]/(1 + m)%N -[n.+1]/(1 + n)%N in M Da *.
pose Mu := ursubmx M; pose Ml := dlsubmx M.
have{Da} Da: ulsubmx M = 1 by rewrite [_ M]mx11_scalar !mxE !lshift0 Da.
pose M1 := - (Ml *m Mu) + drsubmx M.
have [|L uL [R uR [d dvD dM1]]] := IHmn m n M1; first by rewrite -addnS ltnW.
exists (block_mx 1 0 Ml L).
  by rewrite unitmxE det_lblock det_scalar1 mul1r.
exists (block_mx 1 Mu 0 R).
  by rewrite unitmxE det_ublock det_scalar1 mul1r.
exists (1 :: d); set D1 := \matrix_(i, j) _ in dM1.
  by rewrite /= path_min_sorted // => g _; apply: dvd1n.
rewrite [D in _ *m D *m _](_ : _ = block_mx 1 0 0 D1); last first.
  by apply/matrixP=> i j; do 3?[rewrite ?mxE ?ord1 //=; case: splitP => ? ->].
rewrite !mulmx_block !(mul0mx, mulmx0, addr0) !mulmx1 add0r mul1mx -Da -dM1.
by rewrite addNKr submxK.
Qed.

Definition inIntSpan (V : zmodType) m (s : m.-tuple V) v :=
  exists a : int ^ m, v = \sum_(i < m) s`_i *~ a i.

Lemma dec_Qint_span (vT : vectType rat) m (s : m.-tuple vT) v :
  decidable (inIntSpan s v).
Proof.
have s_s (i : 'I_m): s`_i \in <<s>>%VS by rewrite memv_span ?memt_nth.
have s_Zs a: \sum_(i < m) s`_i *~ a i \in <<s>>%VS.
  by rewrite memv_suml // => i _; rewrite -scaler_int memvZ.
case s_v: (v \in <<s>>%VS); last by right=> [[a Dv]]; rewrite Dv s_Zs in s_v.
pose S := \matrix_(i < m, j < _) coord (vbasis <<s>>) j s`_i.
pose r := \rank S; pose k := (m - r)%N; pose Em := erefl m; pose Ek := erefl k.
have Dm: (m = k + r)%N by rewrite subnK ?rank_leq_row.
have [K kerK]: {K : 'M_(k, m) | map_mx intr K == kermx S}%MS.
  pose B := row_base (kermx S); pose d := \prod_ij denq (B ij.1 ij.2).
  exists (castmx (mxrank_ker S, Em) (map_mx numq (intr d *: B))).
  rewrite /k; case: _ / (mxrank_ker S); set B1 := map_mx _ _.
  have ->: B1 = (intr d *: B).
    apply/matrixP=> i j; rewrite 3!mxE mulrC [d](bigD1 (i, j)) // rmorphM mulrA.
    by rewrite -numqE -rmorphM numq_int.
  suffices nz_d: d%:Q != 0 by rewrite !eqmx_scale // !eq_row_base andbb.
  by rewrite intr_eq0; apply/prodf_neq0 => i _; apply: denq_neq0.
have [L _ [G uG [D _ defK]]] := int_Smith_normal_form K.
pose Gud := castmx (Dm, Em) G; pose G'lr := castmx (Em, Dm) (invmx G).
have{K L D defK kerK} kerGu: map_mx intr (usubmx Gud) *m S = 0.
  pose Kl : 'M[rat]_k:= map_mx intr (lsubmx (castmx (Ek, Dm) (K *m invmx G))).
  have{defK} defK: map_mx intr K = row_mx Kl 0 *m map_mx intr Gud.
    rewrite -[K](mulmxKV uG) -{2}[G](castmxK Dm Em) -/Gud.
    rewrite -[K *m _](castmxK Ek Dm) map_mxM map_castmx.
    rewrite -(hsubmxK (castmx _ _)) map_row_mx -/Kl map_castmx /Em.
    set Kr := map_mx _ _; case: _ / (esym Dm) (map_mx _ _) => /= GudQ.
    congr (row_mx _ _ *m _); apply/matrixP=> i j; rewrite !mxE defK mulmxK //=.
    rewrite castmxE mxE big1 //= => j1 _; rewrite mxE /= eqn_leq andbC.
    by rewrite leqNgt (leq_trans (valP j1)) ?mulr0 ?leq_addr.
  have /row_full_inj: row_full Kl; last apply.
    rewrite /row_full eqn_leq rank_leq_row /= -{1}[k](mxrank_ker S).
    rewrite -(eqmxP kerK) defK map_castmx mxrankMfree; last first.
      case: _ / (Dm); apply/row_freeP; exists (map_mx intr (invmx G)).
      by rewrite -map_mxM mulmxV ?map_mx1.
    by rewrite -mxrank_tr tr_row_mx trmx0 -addsmxE addsmx0 mxrank_tr.
  rewrite mulmx0 mulmxA (sub_kermxP _) // -(eqmxP kerK) defK.
  by rewrite -{2}[Gud]vsubmxK map_col_mx mul_row_col mul0mx addr0.
pose T := map_mx intr (dsubmx Gud) *m S.
have{kerGu} defS: map_mx intr (rsubmx G'lr) *m T = S.
  have: G'lr *m Gud = 1%:M by rewrite /G'lr /Gud; case: _ / (Dm); apply: mulVmx.
  rewrite -{1}[G'lr]hsubmxK -[Gud]vsubmxK mulmxA mul_row_col -map_mxM.
  move/(canRL (addKr _))->; rewrite -mulNmx raddfD /= map_mx1 map_mxM /=.
  by rewrite mulmxDl -mulmxA kerGu mulmx0 add0r mul1mx.
pose vv := \row_j coord (vbasis <<s>>) j v.
have uS: row_full S.
  apply/row_fullP; exists (\matrix_(i, j) coord s j (vbasis <<s>>)`_i).
  apply/matrixP=> j1 j2; rewrite !mxE.
  rewrite -(coord_free _ _ (basis_free (vbasisP _))).
  rewrite -!tnth_nth (coord_span (vbasis_mem (mem_tnth j1 _))) linear_sum.
  by apply: eq_bigr => i _; rewrite !mxE (tnth_nth 0) !linearZ.
have eqST: (S :=: T)%MS by apply/eqmxP; rewrite -{1}defS !submxMl.
case Zv: (map_mx denq (vv *m pinvmx T) == const_mx 1).
  pose a := map_mx numq (vv *m pinvmx T) *m dsubmx Gud.
  left; exists [ffun j => a 0 j].
  transitivity (\sum_j (map_mx intr a *m S) 0 j *: (vbasis <<s>>)`_j).
    rewrite {1}(coord_vbasis s_v); apply: eq_bigr => j _; congr (_ *: _).
    have ->: map_mx intr a = vv *m pinvmx T *m map_mx intr (dsubmx Gud).
      rewrite map_mxM /=; congr (_ *m _); apply/rowP=> i; rewrite 2!mxE numqE.
      by have /eqP/rowP/(_ i) := Zv; rewrite !mxE => ->; rewrite mulr1.
    by rewrite -(mulmxA _ _ S) mulmxKpV ?mxE // -eqST submx_full.
  rewrite (coord_vbasis (s_Zs _)); apply: eq_bigr => j _; congr (_ *: _).
  rewrite linear_sum mxE; apply: eq_bigr => i _.
  by rewrite -scaler_int linearZ [a]lock !mxE ffunE.
right=> [[a Dv]]; case/eqP: Zv; apply/rowP.
have ->: vv = map_mx intr (\row_i a i) *m S.
  apply/rowP=> j; rewrite !mxE Dv linear_sum.
  by apply: eq_bigr => i _; rewrite -scaler_int linearZ !mxE.
rewrite -defS -2!mulmxA; have ->: T *m pinvmx T = 1%:M.
  have uT: row_free T by rewrite /row_free -eqST.
  by apply: (row_free_inj uT); rewrite mul1mx mulmxKpV.
by move=> i; rewrite mulmx1 -map_mxM 2!mxE denq_int mxE.
Qed.

