proposition: Lemma acc_gcdP : forall (n:nat) (hn: Acc (fun x y => x < y) n) (a b: R) (hb: n = norm b) (g :R), g %| (acc_gcd hn a hb) = (g %| a) && (g %| b).
proof: Proof. move=> n hn; elim/acc_dep: hn => {}n {}hn hi a b heq g /=. move: (@tool a b). case b0 : (b == 0). - move => _. by rewrite (eqP b0) (dvdr0) andbT. case r0 : ( a %% b == 0). - move => _. by rewrite dvd_mod (eqP r0) dvdr0 andbT. move => h2. rewrite (hi (norm (a %% b)) _ b (a %% b) (refl_equal (norm (a %% b))) g). by rewrite -{1}dvd_mod. 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