proposition: Lemma Rabs_left1 : forall a:R, a <= 0 -> Rabs a = - a.
proof: Proof. intros a H; case H; intros H1. - apply Rabs_left; auto. - rewrite H1; simpl; rewrite Rabs_right; auto with real. Qed.
imports: Rdefinitions Raxioms RIneq R_Ifp