/- Clara L"oh 2021 -/

import tactic          -- standard proof tactics
import data.real.basic -- standards on real numbers

open classical   -- we want to work in classical logic

/-
# A small estimate for absolute values

This is the proof of a simple estimate on absolute values.

-/

lemma simple_estimate
      (x y : real)
      (x_plus_y_1 : x + y = 1)
      (x_geq_y: x ≥ y)
    : (abs x ≥ abs y)
:= 
begin
  -- We first show x ≥ 0 and thus abs x = x:   
  have x_geq_0: x ≥ (0 : real), 
       by {linarith}, -- the linear arithmetic solver auto-proves this
  have abs_x_eq_x: abs x = x, 
       by {rw abs_of_nonneg x_geq_0},       

  -- We now distinguish two cases, 
  -- namely whether y is non-negative or not:
  have case_y_nonneg: y ≥ 0 → abs x ≥ abs y, by
       begin
         assume y_nonneg: 0 ≤ y, 
         calc abs x = x     : by {exact abs_x_eq_x}    
                ... ≥ y     : by {exact x_geq_y} 
                ... = abs y : by {rw abs_of_nonneg y_nonneg},
       end,     

  have case_y_neg: y < 0 → abs x ≥ abs y, by
       begin
         assume y_neg: y < 0,     
         calc abs x = x     : by {exact abs_x_eq_x}
                ... ≥ x - 1 : by {linarith}
                ... = -y    : by {linarith[x_plus_y_1]}
                ... = abs y : by {rw abs_of_neg y_neg},
       end,

  show abs x ≥ abs y, by {finish},     
end