proposition: Lemma abs_ge_0 : forall x, 0 <= abs x.
proof: Proof. intros x. apply Rmult_le_reg_l with 2. by apply Rlt_0_2. rewrite Rmult_0_r -abs_zero -(plus_opp_l x). apply Rle_trans with (1 := abs_triangle _ _). rewrite abs_opp. apply Req_le ; ring. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub