proposition: Lemma dvdp_addl n d m : d %| n -> (d %| m + n) = (d %| m).
proof: Proof. by rewrite addrC; apply: dvdp_addr. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)