proposition: Fact divZ0 m d : d = 0%Z -> divZ m d = 0%Z.
proof: Proof. by move=> ->. Qed.
imports: Coq(ZArith ZifyClasses ZifyInst ZifyBool) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(div choice fintype tuple finfun bigop finset prime) mathcomp(order binomial)