proposition: Lemma Rle_R1_pow: forall (x:R) (m n:nat), 0 <= x <= 1 -> (m <= n)%nat -> x^n <= x^m.
proof: Proof. induction 2; auto with real. simpl. replace (x^m) with (1*x^m) by auto with real. destruct H. apply Rmult_le_compat; trivial. now apply pow_le. Qed.
imports: RTopology SeparatednessAxioms RFuncContinuity UniformTopology ContinuousFactorization Coq(Description Max Psatz ClassicalChoice) ZornsLemma(Proj1SigInjective) UrysohnsLemma