proposition: Lemma Reqdec : forall x:R, {x=0} + {x<>0}.
proof: Proof. intros. induction (total_order_T x 0) as [xneg|xspos]. induction xneg as [xsneg|x0]. right. apply not_eq_sym. apply Rlt_neq. assumption. left. assumption. right. apply Rlt_neq. assumption. Qed.
imports: Reals Coq.Reals.Rtrigo_def Coquelicot.Coquelicot Coquelicot.ElemFct Lra