val lower_bounded_trans (#a: _) {| _: ordered a |} (l: list a) (m1 m2: _)
    : Lemma (requires lower_bounded l m1 /\ leq m2 m1) (ensures lower_bounded l m2)
val lower_bounded_trans (#a: _) {| _: ordered a |} (l: list a) (m1 m2: _)
    : Lemma (requires lower_bounded l m1 /\ leq m2 m1) (ensures lower_bounded l m2)
let rec lower_bounded_trans #a {| _ : ordered a |} (l: list a) m1 m2:
  Lemma (requires lower_bounded l m1 /\ leq m2 m1) (ensures lower_bounded l m2)
= match l with
  | [] -> ()
  | t::q -> (transitivity m2 m1 t; lower_bounded_trans q m1 m2)
(*
   Copyright 2023 Microsoft Research
   Licensed under the Apache License, Version 2.0 (the "License");
   you may not use this file except in compliance with the License.
   You may obtain a copy of the License at
       http://www.apache.org/licenses/LICENSE-2.0
   Unless required by applicable law or agreed to in writing, software
   distributed under the License is distributed on an "AS IS" BASIS,
   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
   See the License for the specific language governing permissions and
   limitations under the License.
*)

module LeftistHeap

// -----------------------------------------------------------------
// Elimination rules for the ordered type class, and instantiations
// -----------------------------------------------------------------

let gt (#t: eqtype) {| _ : ordered t |} (a b: t) =
  leq b a && a <> b

let transitivity #a {| p : ordered a |} (x y z: a):
  Lemma (requires leq x y /\ leq y z)
  (ensures leq x z)
= p.properties

let reflexivity #a {| p : ordered a |} (x: a):
  Lemma (ensures leq x x)
= p.properties

let antisymmetry (#a: eqtype) {| p : ordered a |} (x y: a):
  Lemma (requires leq x y /\ leq y x) (ensures x = y)
= p.properties

let total_order (#a: eqtype) {| p : ordered a |} (x y: a):
  Lemma (ensures leq x y \/ leq y x)
= p.properties

instance ints_leq : ordered int =
{
  leq = (<=);
  properties = ()
}

instance nats_leq : ordered nat =
{
  leq = (<=);
  properties = ()
}

// -----------------------------------------------------------------
// Useful functions and lemmas for lists
// -----------------------------------------------------------------

let delta (#a: eqtype) (x y:a): GTot int = (if x = y then 1 else 0)

let rec count (#a: eqtype) (l: list a) y: GTot nat =
  match l with
  | [] -> 0
  | t::q -> delta t y + count q y

let rec lower_bounded #a {| _ : ordered a |} (l: list a) m: GTot bool =
  match l with
  | [] -> true
  | t::q -> leq m t && lower_bounded q m
/
prims.fst.checked FStar.Tactics.Typeclasses.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Classical.Sugar.fsti.checked FStar.Calc.fsti.checked
LeftistHeap.fst
{| _: LeftistHeap.ordered a |} -> l: Prims.list a -> m1: a -> m2: a
  -> FStar.Pervasives.Lemma (requires LeftistHeap.lower_bounded l m1 /\ LeftistHeap.leq m2 m1)
      (ensures LeftistHeap.lower_bounded l m2)
Prims.eqtype LeftistHeap.ordered Prims.list LeftistHeap.lower_bounded_trans Prims.unit LeftistHeap.transitivity Prims.l_and Prims.b2t LeftistHeap.lower_bounded LeftistHeap.leq Prims.squash Prims.Nil FStar.Pervasives.pattern
let rec lower_bounded_trans #a {| _: ordered a |} (l: list a) m1 m2
    : Lemma (requires lower_bounded l m1 /\ leq m2 m1) (ensures lower_bounded l m2) =
  
match l with
| [] -> ()
| t :: q ->
  (transitivity m2 m1 t;
    lower_bounded_trans q m1 m2)