proposition: Lemma Qpower_plus' : forall a n m, (n+m <> 0)%Z -> a^(n+m) == a^n*a^m.
proof: Proof. intros a n m H. destruct (Qeq_dec a 0)as [X|X]. - rewrite X. rewrite Qpower_0 by assumption. destruct n; destruct m; try (elim H; reflexivity); simpl; repeat rewrite Qpower_positive_0; ring_simplify; reflexivity. - apply Qpower_plus. assumption. Qed.
imports: Zpow_facts Qfield Qreduction