proposition: Lemma prod_norm_eq_zero : forall x : U * V, prod_norm x = 0 -> x = zero.
proof: Proof. intros [xu xv] H. apply sqrt_eq_0 in H. rewrite !(pow_Rsqr _ 1) !pow_1 in H. apply Rplus_sqr_eq_0 in H. destruct H as [H1 H2]. apply norm_eq_zero in H1. apply norm_eq_zero in H2. simpl in H1, H2. now rewrite H1 H2. apply Rplus_le_le_0_compat ; apply pow2_ge_0. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub