proposition: Lemma prod_norm_compat1 : forall (x y : U * V) (eps : R), prod_norm (minus y x) < eps -> ball x eps y.
proof: Proof. intros [xu xv] [yu yv] eps H. generalize (Rle_lt_trans _ _ _ (proj1 (sqrt_plus_sqr _ _)) H). rewrite -> !Rabs_pos_eq by apply norm_ge_0. intros H'. split ; apply norm_compat1 ; apply Rle_lt_trans with (2 := H'). apply Rmax_l. apply Rmax_r. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub