proposition: Lemma X_le_dec_trans : forall x y z, X_le_dec x y = true -> X_le_dec y z = true -> X_le_dec x z = true.
proof: Proof. unfold X_le_dec; intros; destruct (X.compare x y); destruct (X.compare y z); intuition. - apply X_le_sound; right; eapply X.lt_trans; eauto. - apply X_le_sound; right; eapply Raw.Proofs.L.PX.MO.lt_eq; eauto. - apply X_le_sound; right; eapply Raw.Proofs.L.PX.MO.eq_lt; eauto. - apply X_le_sound; left; eapply X.eq_trans; 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