Load "basics.tt";

Data le : (m,n:Nat)* =
    leO : (n:_)(le O n)
  | leS : (m,n:_)(p:le m n)(le (S m) (S n));

Match leSuc : (m,n:Nat)(p:le m n)(le m (S n)) =
    leSuc _ _ (leO _) = leO _
  | leSuc _ _ (leS _ _ p) = leS _ _ (leSuc _ _ p);

Match leSym : (m:Nat)(le m m) =
    leSym O = leO _
  | leSym (S k) = leS _ _ (leSym k);

Match lePlus : (m,n:Nat)(le m (plus m n)) =
    lePlus O n = leO _
  | lePlus (S k) n = leS _ _ (lePlus k n);

Data Compare : (m,n:Nat)* =
    cmpLT : (k,m:Nat)(Compare m (plus m (S k)))
  | cmpEQ : (n:Nat)(Compare n n)
  | cmpGT : (k,n:Nat)(Compare (plus n (S k)) n);

Match Partial compareAux : (m,n:Nat)(Compare m n)->(Compare (S m) (S n)) =
    compareAux _ _ (cmpLT k _) = cmpLT k _
  | compareAux _ _ (cmpEQ n) = cmpEQ _
  | compareAux _ _ (cmpGT k _) = cmpGT k _;

Match compare : (m,n:Nat)(Compare m n) =
    compare O (S k) = cmpLT _ O
  | compare O O = cmpEQ _
  | compare (S k) O = cmpGT _ O
  | compare (S x) (S y) = compareAux _ _ (compare x y);

Match mkLTaux : (m,n:Nat)(Compare m n)->(Maybe (le m n)) =
    mkLTaux _ _ (cmpLT k m) = just _ (lePlus m (S k))
  | mkLTaux _ _ (cmpEQ m) = just _ (leSym m)
  | mkLTaux _ _ (cmpGT k m) = nothing _;

mkLT = [m,n:Nat](mkLTaux _ _ (compare m n));

isBounded : (n,min,max:Nat)(Maybe (And (le min n) (le n max)));
intros;
induction mkLT min n;
refine nothing;
intros;
induction mkLT n max;
refine nothing;
intros;
refine just;
refine and_intro;
refine a;
refine a0;
Qed;