proposition: Lemma Rmax_using_Rabs x y : Rmax x y = (x + y + Rabs (x-y))*(1/2).
proof: Proof. destruct (classic (x <= y)). - rewrite Rmax_right; try assumption. rewrite Rabs_minus_sym. rewrite Rabs_pos_eq; lra. - rewrite Rmax_left; try lra. rewrite Rabs_pos_eq; lra. Qed.
imports: RTopology ProductTopology Homeomorphisms ContinuousFactorization Coq(FunctionalExtensionality Lra ProofIrrelevance) ZornsLemma(EnsembleProduct EnsemblesTactics)