proposition: Lemma pow_div_l : forall a b c, b~=0 -> a mod b == 0 -> (a/b)^c == a^c / b^c.
proof: Proof. intros a b c Hb H. apply div_unique with 0. - generalize (pow_nonzero b c Hb) (le_0_l (b^c)); order'. - nzsimpl. rewrite <- pow_mul_l. f_equiv. now apply div_exact. Qed.
imports: Bool NAxioms NSub NPow NDiv NParity NLog