proposition: Lemma Q3c : forall n, pow_n A n = mult P (mult (pow_n D n) P').
proof: Proof. elim => /= [ | n IH]. rewrite mult_one_l. apply sym_eq, Q3a. by rewrite -{1}Q3b !mult_assoc (proj1 Q3a) mult_one_l -!mult_assoc IH. Qed.
imports: Coq(Reals Psatz ssreflect) Coquelicot(Hierarchy PSeries Rbar Lim_seq)