Commit e7c5e6a6 authored by Nicola Botta's avatar Nicola Botta
Browse files


parent 781afc3c
import Data.So
public export
data LTE : Double -> Double -> Type where
MkLTE : {x : Double} -> {y : Double} -> So (x <= y) -> LTE x y
||| Postulate LTE to be monotone w.r.t. addition
public export
monotonePlusLTE : {a, b, c, d : Double} ->
a `LTE` b -> c `LTE` d -> a + c `LTE` b + d
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment