proposition: Lemma coordnormb : forall x:R, forall y:R, y<>0 -> 0<sqrt(x^2+y^2)+x.
proof: Proof. intros. rewrite<-(Ropp_involutive x) at 2. apply Rlt_Rminus. apply coordnorm. assumption. Qed.
imports: Reals Coq.Reals.Rtrigo_def Coquelicot.Coquelicot Coquelicot.ElemFct Lra