proposition: Lemma normspos : forall x:R, forall y:R, x<>0 -> 0<x^2+y^2.
proof: Proof. intros. do 2 rewrite<-Rsqr_pow2. apply Rplus_lt_le_0_compat. apply Rsqr_pos_lt. assumption. apply Rle_0_sqr. Qed.
imports: Reals Coq.Reals.Rtrigo_def Coquelicot.Coquelicot Coquelicot.ElemFct Lra