proposition: Lemma Cpow_mult_l a b n : (a*b)^n = a^n * b^n.
proof: Proof. induction n; simpl. now rewrite Cmult_1_l. rewrite IHn. rewrite Cmult_assoc. rewrite <- (Cmult_assoc a b _). rewrite (Cmult_comm b _). now rewrite !Cmult_assoc. Qed.
imports: Coq(Reals ssreflect) Rcomplements Rbar Continuity Derive Hierarchy