proposition: Lemma modn_partP n a b : 0 < n -> reflect (forall p : nat, p \in \pi(n) -> a = b %[mod n`_p]) (a == b %[mod n]).
proof: Proof. move=> n_gt0; wlog le_b_a: a b / b <= a. move=> IH; case: (leqP b a) => [|/ltnW] /IH {IH}// IH. by rewrite eq_sym; apply: (iffP IH) => eqab p /eqab. rewrite eqn_mod_dvd //; apply: (iffP (dvdn_partP _ n_gt0)) => eqab p /eqab; by rewrite -eqn_mod_dvd // => /eqP. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(fintype div bigop)