proposition: Lemma congr_eqd b d a c : a %= b -> c %= d -> (a %= c) = (b %= d).
proof: Proof. move=> ab cd; apply/idP/idP=> [ac|bd]. by rewrite eqd_sym in ab; rewrite (eqd_trans (eqd_trans ab ac) cd). by rewrite eqd_sym in cd; rewrite (eqd_trans ab (eqd_trans bd cd)). 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