proposition: Lemma eqmodP x y : reflect (x = y %[mod qT]) (eD x y).
proof: Proof. by apply: (iffP (pi_DC _ _)); rewrite !unlock. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice) mathcomp(seq fintype)