proposition: Theorem leb_total : forall a1 a2 : t, leb a1 a2 = true \/ leb a2 a1 = true.
proof: Proof. unfold t; intros; intuition; unfold leb; simpl. case_eq (Compare_dec.leb b b0); intuition. case_eq (Compare_dec.leb b0 b); intuition. apply leb_iff_conv in H; apply leb_iff_conv in H0. omega. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.Sorting.Mergesort Coq.Structures.Orders Coq.Arith.Arith Coq.Structures.OrderedType Coq.Structures.OrderedTypeEx Coq.Strings.String Coq.FSets.FMapAVL Fiat.Common.String_as_OT Fiat.Common.Tactics.CacheStringConstant Fiat.QueryStructure.Specification.Representation.QueryStructureNotations Fiat.QueryStructure.Implementation.Operations Fiat.QueryStructure.Implementation.DataStructures.BagADT.QueryStructureImplementation Fiat.QueryStructure.Implementation.DataStructures.BagADT.IndexSearchTerms Fiat.QueryStructure.Automation.Common