proposition: Lemma dvdp_subl d m n : d %| n -> (d %| m - n) = (d %| m).
proof: Proof. by move/dvdp_addl<-; rewrite subrK. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)