proposition: Lemma pow_div_l : forall a b c, b~=0 -> 0<=c -> a mod b == 0 -> (a/b)^c == a^c / b^c.
proof: Proof. intros a b c Hb Hc H. rewrite (div_mod a b Hb) at 2. rewrite H, add_0_r, pow_mul_l, mul_comm, div_mul. { reflexivity. } now apply pow_nonzero. Qed.
imports: Bool ZAxioms ZMulOrder ZPow ZDivFloor ZSgnAbs ZParity NZLog