Q/ratio/rtimes.ma Q/fraction/ftimes.ma Q/ratio/rinv.ma
Q/fraction/fraction.ma Z/compare.ma nat/factorization.ma
Q/fraction/finv.ma Q/fraction/fraction.ma Z/plus.ma
-Q/fraction/ftimes.ma Q/fraction/finv.ma Q/ratio/ratio.ma
+Q/fraction/ftimes.ma Q/fraction/finv.ma Q/nat_fact/times.ma Q/ratio/ratio.ma Z/times.ma
+Q/fraction/numerator_denominator.ma Q/fraction/finv.ma
+Q/nat_fact/times.ma nat/factorization.ma
datatypes/compare.ma
datatypes/constructors.ma logic/equality.ma
datatypes/bool.ma higher_order_defs/functions.ma logic/equality.ma