proposition: Lemma d'_eq_0 : forall x y : ℝ, d_discrete_R x y = 0 -> (Reqb x y) = true.
proof: Proof. Take x, y : ℝ. Assume that (d_discrete_R x y = 0). Either (x = y) or (x ≠ y). + Case (x = y). By Req_true we conclude that (Reqb x y = true). + Case (x ≠ y). It holds that ((if Reqb(x, y) then 0 else 3) = 0) (i). rewrite (Req_false x y H) in i. Contradiction. Qed.
imports: Coq.Reals.Reals Reals.ROrderedType micromega.Lra Tactics Automation Libs.Reals Notations