fact: Definition egcdr3 (a b c : R) := let: (g',u1,vv1,b1,c1) := egcdr b c in let: (g,u,v,a1,g1) := egcdr a g' in (g, u, v * u1, v * vv1, a1, b1 * g1,c1 * g1).
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq path) mathcomp(ssralg fintype matrix mxalgebra bigop zmodp perm choice) dvdring mxstructure minor stronglydiscrete coherent edr