fact: Definition ltb (x y : t) : bool := (t_to_Z x <? t_to_Z y)%Z || (((t_to_Z x =? t_to_Z y)%Z) && ((fst x <? fst y) || ((fst x =? fst y) && (snd x <? snd y)))).
imports: Coq.QArith.QArith Coq.Structures.Orders Coq.micromega.Lia Coq.Bool.Bool Coq.Sorting.Mergesort Coq.Lists.List Coq.ZArith.ZArith PerformanceExperiments.Sandbox