proposition: Lemma prod_norm_compat2 : forall (x y : U * V) (eps : posreal), ball x eps y -> prod_norm (minus y x) < prod_norm_factor * eps.
proof: Proof. intros [xu xv] [yu yv] eps [Bu Bv]. apply Rle_lt_trans with (1 := proj2 (sqrt_plus_sqr _ _)). simpl. rewrite Rmult_assoc. apply Rmult_lt_compat_l. apply sqrt_lt_R0. apply Rlt_0_2. rewrite -> !Rabs_pos_eq by apply norm_ge_0. rewrite Rmax_mult. apply Rmax_case. apply Rlt_le_trans with (2 := Rmax_l _ _). now apply norm_compat2. apply Rlt_le_trans with (2 := Rmax_r _ _). now apply norm_compat2. apply Rlt_le. apply cond_pos. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub