proposition: Lemma eq_dec : forall x y : V, { x = y } + { x <> y }.
proof: Proof. intros x y. destruct (Req_EM_T (norm (minus y x)) 0) as [H|H]. - left. apply plus_reg_r with (opp x). rewrite plus_opp_r. now apply eq_sym, norm_eq_zero. - right. contradict H. rewrite H minus_eq_zero. apply norm_zero. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub