-metric_lattice.ma lattice.ma metric_space.ma
+metric_lattice.ma excess.ma lattice.ma metric_space.ma
metric_space.ma ordered_divisible_group.ma
-sandwich.ma nat/orders.ma nat/plus.ma tend.ma
+sandwich.ma metric_lattice.ma nat/orders.ma nat/plus.ma tend.ma
premetric_lattice.ma lattice.ma metric_space.ma
ordered_group.ma group.ma
divisible_group.ma group.ma nat/orders.ma
ordered_divisible_group.ma divisible_group.ma nat/orders.ma nat/times.ma ordered_group.ma
sequence.ma excess.ma
constructive_connectives.ma logic/connectives.ma
-lattice.TF.ma excess.ma lattice.ma nat/nat.ma
group.ma excess.ma
prevalued_lattice.ma ordered_group.ma
excess.ma constructive_connectives.ma constructive_higher_order_relations.ma higher_order_defs/relations.ma nat/plus.ma
sandwich_corollary.ma sandwich.ma
Q_is_orded_divisble_group.ma Q/q.ma ordered_divisible_group.ma
-limit.ma excess.ma infsup.ma tend.ma
+limit.ma excess.ma infsup.ma metric_lattice.ma tend.ma
lattice.ma excess.ma
-tend.ma metric_lattice.ma nat/orders.ma sequence.ma
+tend.ma metric_space.ma nat/orders.ma sequence.ma
constructive_higher_order_relations.ma constructive_connectives.ma higher_order_defs/relations.ma
infsup.ma excess.ma sequence.ma
constructive_pointfree/lebesgue.ma constructive_connectives.ma metric_lattice.ma sequence.ma