proposition: Lemma eqmod_equivalence (R:= graph_on (fun a b => a = b %c[mod B]) Nat): equivalence_on R Nat.
proof: Proof. split; last by apply: graph_on_sr => a. apply: equivalence_from_rel; split. by move => a b ab. by move => b a c; rewrite /eqmod => -> ->. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)