Insertion in sorted binary tree

module Bintree_insert

  use import bintree.Tree
  use import bintree.Size
  use import bintree.Inorder
  use import bintree.InorderLength
  use import int.Int
(*-------------------------------*)
predicate memt (t : tree int) (k : int) =
    match t with
    | Empty -> false
    | Node t1 x t2 -> (k = x) \/ memt t1 k \/ memt t2 k
    end

  predicate leq_tree (x : int) (t : tree int) =
    forall k : int. memt t k -> k <= x

  predicate geq_tree (x : int) (t : tree int) =
    forall k : int. memt t k -> x <= k

  predicate sorted (t : tree int) =
    match t with
    | Empty -> true
    | Node t1 x t2 -> sorted t1 /\ sorted t2 /\ leq_tree x t1 /\ geq_tree x t2
    end
(*-------------------------------*)

  let rec add (t : tree int) (v : int) : tree int =
    requires {sorted t}
    ensures {(sorted result) /\ (forall x : int. memt result x -> (memt t x \/ x = v)) }
    match t with
     | Empty -> Node (Empty) v (Empty)
     | Node t1 x t2 ->
       if v <= x then Node (add t1 v) x t2 else Node t1 x (add t2 v)
    end

end