val reflexivity (#a: _) {| p: ordered a |} (x: a) : Lemma (ensures leq x x)
val reflexivity (#a: _) {| p: ordered a |} (x: a) : Lemma (ensures leq x x)
let reflexivity #a {| p : ordered a |} (x: a):
  Lemma (ensures leq x x)
= p.properties
(*
   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
/
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
{| p: LeftistHeap.ordered a |} -> x: a -> FStar.Pervasives.Lemma (ensures LeftistHeap.leq x x)
Prims.eqtype LeftistHeap.ordered LeftistHeap.__proj__Mkordered__item__properties Prims.unit Prims.l_True Prims.squash Prims.b2t LeftistHeap.leq Prims.Nil FStar.Pervasives.pattern
let reflexivity #a {| p: ordered a |} (x: a) : Lemma (ensures leq x x) =
  
p.properties