proposition: Lemma missing_pow_mult: forall (x y:R) (n:nat), (x*y)^n = x^n * y^n.
proof: Proof. induction n. - lra. - simpl. rewrite IHn. lra. Qed.
imports: RTopology SeparatednessAxioms RFuncContinuity UniformTopology ContinuousFactorization Coq(Description Max Psatz ClassicalChoice) ZornsLemma(Proj1SigInjective) UrysohnsLemma