proposition: Lemma pow_sub_r : forall a b c, a~=0 -> 0<=c<=b -> a^(b-c) == a^b / a^c.
proof: Proof. intros a b c Ha (H,H'). rewrite <- (sub_simpl_r b c) at 2. rewrite pow_add_r; trivial. - rewrite div_mul. { reflexivity. } now apply pow_nonzero. - now apply le_0_sub. Qed.
imports: Bool ZAxioms ZMulOrder ZPow ZDivFloor ZSgnAbs ZParity NZLog