proposition: Theorem powerRZ_add : forall (e : R) (n m : Z), e <> 0%R -> powerRZ e (n + m) = (powerRZ e n * powerRZ e m)%R.
proof: Proof. intros e n m; case n; case m; simpl in |- *; auto with real. intros n1 m1; rewrite nat_of_P_plus_morphism; auto with real. intros n1 m1. rewrite Z.pos_sub_spec; unfold Pos.compare. CaseEq (Pcompare m1 n1 Datatypes.Eq); simpl in |- *; auto with real. intros H' H'0; rewrite Pcompare_Eq_eq with (1 := H'); auto with real. intros H' H'0; rewrite (nat_of_P_minus_morphism n1 m1); auto with real. rewrite (pow_RN_plus e (nat_of_P n1 - nat_of_P m1) (nat_of_P m1)); auto with real. rewrite Nat.sub_add. rewrite Rinv_mult_distr; auto with real. rewrite Rinv_involutive; auto with real. apply Nat.lt_le_incl. apply nat_of_P_lt_Lt_compare_morphism; auto. apply ZC2; auto. intros H' H'0; rewrite (nat_of_P_minus_morphism m1 n1); auto with real. rewrite (pow_RN_plus e (nat_of_P m1 - nat_of_P n1) (nat_of_P n1)); auto with real. rewrite Nat.sub_add; auto with real. apply Nat.lt_le_incl. change (nat_of_P m1 > nat_of_P n1) in |- *. apply nat_of_P_gt_Gt_compare_morphism; auto. intros n1 m1. rewrite Z.pos_sub_spec; unfold Pos.compare. CaseEq (Pcompare n1 m1 Datatypes.Eq); simpl in |- *; auto with real. intros H' H'0; rewrite Pcompare_Eq_eq with (1 := H'); auto with real. intros H' H'0; rewrite (nat_of_P_minus_morphism m1 n1); auto with real. rewrite (pow_RN_plus e (nat_of_P m1 - nat_of_P n1) (nat_of_P n1)); auto with real. rewrite Nat.sub_add. rewrite Rinv_mult_distr; auto with real. apply Nat.lt_le_incl. apply nat_of_P_lt_Lt_compare_morphism; auto. apply ZC2; auto. intros H' H'0; rewrite (nat_of_P_minus_morphism n1 m1); auto with real. rewrite (pow_RN_plus e (nat_of_P n1 - nat_of_P m1) (nat_of_P m1)); auto with real. rewrite Nat.sub_add; auto with real. apply Nat.lt_le_incl. change (nat_of_P n1 > nat_of_P m1) in |- *. apply nat_of_P_gt_Gt_compare_morphism; auto. intros n1 m1; rewrite nat_of_P_plus_morphism; auto with real. intros H'; rewrite pow_add; auto with real. apply Rinv_mult_distr; auto. apply pow_NR0; auto. apply pow_NR0; auto. Qed.
imports: Reals ZArith List PeanoNat Psatz