lean2/library/data/nat/default.lean

/-
Copyright (c) 2014 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Jeremy Avigad
-/
import .basic .order .sub .div .bquant .sqrt .pairing .power
refactor(library/data/nat): merge comm_semiring, make minor fixes 2015-02-01 14:55:12 +00:00			`/-`
			`Copyright (c) 2014 Microsoft Corporation. All rights reserved.`
			`Released under Apache 2.0 license as described in the file LICENSE.`
			`Author: Jeremy Avigad`
			`-/`
theorem(library/data/countable): prove that the product of two countable types is countable 2015-04-15 03:39:58 +00:00			`import .basic .order .sub .div .bquant .sqrt .pairing .power`