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