proposition: Lemma eqd_dvd c d a b : a %= c -> b %= d -> (a %| b) = (c %| d).
proof: Proof. rewrite !eqd_def; case/andP=> ac ca; case/andP=> bd db. apply/idP/idP=> [ab|cd]; first exact: (dvdr_trans ca (dvdr_trans ab bd)). exact: (dvdr_trans ac (dvdr_trans cd db)). 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