proposition: Lemma divzMA_ge0 (m n p : int) : (0 <= n)%R -> (m %/ (n * p))%Z = ((m %/ n) %/ p)%Z.
proof: Proof. nia. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(div choice fintype tuple finfun bigop finset prime) mathcomp(binomial ssralg countalg ssrnum ssrint rat intdiv) mathcomp(zify)