proposition: Theorem X_le_sound : forall x y, X_le_dec x y = true <-> X.eq x y \/ X.lt x y.
proof: Proof. intros x y; unfold X_le_dec. destruct (X.compare x y); intuition. - apply X.lt_not_eq in l; eauto; intuition. - apply Raw.Proofs.L.PX.MO.lt_le in l; eauto. Qed.
imports: Fiat.QueryStructure.Implementation.DataStructures.Bags.BagsInterface Fiat.QueryStructure.Implementation.DataStructures.Bags.BagsProperties Coq.Arith.PeanoNat Coq.FSets.FMapInterface Coq.FSets.FMapFacts Coq.FSets.FMapAVL Fiat.Common Fiat.Common.List.ListFacts Fiat.Common.List.FlattenList Fiat.Common.SetEqProperties Fiat.Common.FMapExtensions Fiat.Common.List.PermutationFacts