proposition: Lemma enc_mod_rel_is_equiv : equiv_class_of (enc_mod_rel r).
proof: Proof. split => [x|x y|y x z]; rewrite !encModRelE //; first by rewrite equiv_sym. by move=> exy /(equiv_trans exy). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice) mathcomp(seq fintype)