proposition: Lemma coordnorm : forall x:R, forall y:R, y<>0 -> -x<sqrt(x^2+y^2).
proof: Proof. intros. apply (Rle_lt_trans _ (Rabs x)). rewrite<-Rabs_Ropp. apply Rle_abs. rewrite<-sqrt_Rsqr_abs. apply sqrt_lt_1_alt. split. apply Rle_0_sqr. repeat rewrite<-Rsqr_pow2. apply Rminus_gt. unfold Rminus. rewrite Rplus_comm. rewrite<-Rplus_assoc. Rsimpl. apply Rlt_0_sqr. assumption. Qed.
imports: Reals Coq.Reals.Rtrigo_def Coquelicot.Coquelicot Coquelicot.ElemFct Lra