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