proposition: Lemma eqn_dvd m n : (m == n) = (m %| n) && (n %| m).
proof: Proof. case: m n => [|m] [|n] //; apply/idP/andP => [/eqP -> //| []]. by rewrite eqn_leq => Hmn Hnm; do 2 rewrite dvdn_leq //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq)