Require Import Arith.Bool_nat.
Require Import Arith.Euclid.
Require Import Bool.BoolEq.
Require Import Bool.DecBool.
Require Import Bool.IfProp.
Require Import Classes.CEquivalence.
Require Import Classes.DecidableClass.
Require Import Classes.EquivDec.
Require Import Classes.Morphisms_Relations.
Require Import Classes.SetoidDec.
(*Require Import Compat.Coq84.
Require Import Compat.Coq85.*)
Require Import FSets.FMapFullAVL.
Require Import FSets.FMaps.
Require Import FSets.FSets.
Require Import FSets.FSetToFiniteSet.
Require Import Init.Prelude.
Require Import Lists.ListSet.
Require Import Lists.ListTactics.
Require Import Logic.Berardi.
Require Import Logic.ClassicalChoice.
Require Import Logic.ClassicalDescription.
Require Import Logic.ClassicalEpsilon.
Require Import Logic.ConstructiveEpsilon.
Require Import Logic.Diaconescu.
Require Import Logic.Epsilon.
Require Import Logic.ExtensionalityFacts.
Require Import Logic.IndefiniteDescription.
Require Import Logic.SetIsType.
Require Import Logic.WKL.
(*Require Import MMaps.MMapAVL.
Require Import MMaps.MMaps.*)
Require Import MSets.MSetRBT.
Require Import MSets.MSets.
Require Import MSets.MSetToFiniteSet.
Require Import NArith.Ndist.
Require Import Numbers.Cyclic.Abstract.NZCyclic.
Require Import Numbers.Cyclic.ZModulo.ZModulo.
Require Import Numbers.Integer.Binary.ZBinary.
Require Import Numbers.Integer.NatPairs.ZNatPairs.
Require Import Numbers.NatInt.NZDomain.
Require Import Numbers.Natural.Abstract.NDefOps.
Require Import Numbers.Natural.Abstract.NIso.
Require Import Numbers.Natural.Binary.NBinary.
Require Import Numbers.Rational.BigQ.BigQ.
Require Import PArith.PArith.
Require Import QArith.Qabs.
Require Import QArith.Qreals.
Require Import QArith.Qround.
Require Import Reals.Reals.
Require Import Reals.Rlogic.
Require Import Reals.Rminmax.
Require Import Sets.Integers.
Require Import Sets.Relations_3_facts.
Require Import Sets.Uniset.
Require Import Sorting.Heap.
Require Import Sorting.PermutEq.
Require Import Strings.String.
Require Import Unicode.Utf8.
Require Import Wellfounded.Wellfounded.
Require Import ZArith.Zdigits.
Require Import ZArith.Zeuclid.
Require Import ZArith.Zpow_alt.
Require Import ZArith.Zquot.
Require Import ZArith.Zsqrt_compat.
Require Import ZArith.Zwf.

From Hammer Require Import Hammer.

Hammer_export Dir "coq_export".
