proposition: Lemma gcdP : forall d a b, d %| gcd a b = (d %| a) && (d %| b).
proof: Proof. move=> d a b; rewrite /gcd. wlog nba: a b / norm b <= norm a=>[hwlog|]. case: ltnP=> nab. by move/hwlog:(ltnW nab); rewrite ltnNge (ltnW nab) /= andbC. by move/hwlog:(nab); rewrite ltnNge nab. rewrite ltnNge nba /=. have [-> | a0] := eqVneq a 0; first by rewrite dvdr0. move: (norm a) {-1 3}a nba a0=> n {}a hn a0. elim: n {-2}n (leqnn n) a b hn a0 => [|k ihk] n hk a b hn a0. move: hk hn; rewrite leqn0; move/eqP->; rewrite leqn0. by move/eqP/norm_eq0->; rewrite modr0 (negbTE a0) dvdr0 andbT. move: hk hn; rewrite leq_eqVlt; case/orP; last first. by rewrite ltnS=> hnk nb; rewrite ihk. move/eqP->; rewrite dvd_mod. case: eqP => [->|_]; first by rewrite dvdr0 andbT. have [-> | b0] := eqVneq b 0. rewrite !modr0 dvdr0 /=. by case: k {ihk}=> [|k]; rewrite mod0r eqxx. by move=> nb; rewrite ihk // -ltnS (leq_trans (mod_spec _ _)). Qed.
imports: HB(structures) Coq(ssreflect ssrfun ssrbool Arith.Wf_nat) mathcomp(eqtype ssrnat div seq path) mathcomp(ssralg fintype perm tuple choice generic_quotient) mathcomp(matrix bigop zmodp mxalgebra poly) stronglydiscrete