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