fact: Definition inrange_priq (priq : list Z) := Forall (fun x => Int.min_signed <= x <= inf + 1) priq.
imports: VST.floyd.proofauto CertiGraph.lib.find_lemmas CertiGraph.priq.is_empty_lemmas CertiGraph.priq.priq_arr