proposition: Lemma Rabs_left1_with_minus : forall a b : R, 0 < a -> b = -a -> Rabs (b) = a.
proof: Proof. intros a b a_gt_0 b_eq_min_a. rewrite b_eq_min_a. unfold Rabs. destruct (Rcase_abs(-a)). - apply Ropp_involutive. - assert (- a < 0). + rewrite<- Ropp_0. apply Ropp_lt_contravar. assumption. + pose proof (Rlt_not_ge (-a) 0 H). contradiction. Qed.
imports: Lra Coq.Reals.Reals Reals.ROrderedType Notations