namespace http://mathhub.info/MitM/core/arithmetics 

import base http://mathhub.info/MitM/Foundation 

theory NaturalNumbers : base:?Logic =
	include ☞base:?NatLiterals 

	succ : ℕ ⟶ ℕ  # Succ 1 prec 5  = [n] succ_nat_lit n 

	axiom_succ1 : {x} ⊦ 0 ≠ Succ x 
	axiom_succ2 : {x:ℕ,y:ℕ} ⊦ Succ x ≐ Succ y ⟶ ⊦ x ≐ y 
	axiom_Induction: {A : ℕ ⟶ bool} ⊦ A 0 ⟶ ({x}⊦ A x ⟶ ⊦ A (Succ x)) ⟶ {x} ⊦ A x 


	
theory NaturalArithmetics : base:?Logic =
	include ?NaturalNumbers 
	include ☞base:?DescriptionOperator 

	/T Addition ❙
	addition : ℕ ⟶ ℕ ⟶ ℕ  # 1 + 2 prec 15  = plus_nat_lit 
	axiom_plus1 : {x} ⊦ x + 0 ≐ x  # axiom_plus1 
	axiom_plus2 : {x,y} ⊦ x + Succ y ≐ Succ (x + y) 
	
	/T Subtraction ❙
	subtraction : {n : ℕ, m : ℕ, p : ⊦ ∃! [x : ℕ] m + x ≐ n}ℕ  = [n,m,p] ι [x: ℕ] m + x ≐ n  # 1 - 2 %I3 prec 15 
	// TODO proof arguments are in the way ❙
	// theorem_sub1: ⊦ ∀[n] n - zero ≐ n ❙
	// theorem_sub2: ⊦ ∀[n] ∀[m] m ≤ n ⇒ (S n) - (S m) ≐ n - m ❙
	
	/T Multiplication ❙
	multiplication : ℕ ⟶ ℕ ⟶ ℕ  # 1  2 prec 25  = times_nat_lit 
	axiom_times1 : {x : ℕ} ⊦ x ⋅ 1 ≐ x 
	axiom_times2 : {x,y} ⊦ x ⋅ Succ y ≐ x + x ⋅ y 
	axiom_times3 : {x: ℕ} ⊦ x ⋅ 0 ≐ 0 ∧ 0 ⋅ x ≐ 0 
	
	/T Division ❙
	divides : ℕ ⟶ ℕ ⟶ bool  = [n,m] ∃! [r : ℕ] n ⋅ r ≐ m  # 1 | 2 prec 105 
	div : {n : ℕ, m : ℕ, p : ⊦ ∃! [r : ℕ] n ⋅ r ≐ m} ℕ  = [n,m,p] ι ([r : ℕ] n ⋅ r ≐ m)  # 1 / 2 %I3 prec 105 
	// theorem_div1: ⊦ ∀[n] ¬ (n ≐ 0) ⇒ zero / n ≐ zero ❙
	// theorem_div2: ⊦ ∀[n] ∀[m] ¬(m ≐ zero) ∧ (m | n) ⇒ n / m ≐ S ((n - m) / m) ❙
	
	/T Exponentiation ❙
	exponentiation : ℕ ⟶ ℕ ⟶ ℕ  # 1 ^ 2 prec 35 
	axiom_exp1 : {x} ⊦ x ^ 0 ≐ 1 
	axiom_exp2 : {x,y} ⊦ x ^ Succ y ≐ x ⋅ x ^ y 
	
	/T Roots ❙
	root : {n : ℕ, m : ℕ, p : ⊦ ∃![x] x^m ≐ n}ℕ  = [n,m,p] ι [x] x^m ≐ n   # 2  1 %I3 prec 35
	squareRoot : {n : ℕ, p : ⊦ ∃![m] m^2 ≐ n}ℕ  = [n,p] 2 √ n  #  1 %I2 prec 35 
	
	/T Order ❙
	leq : ℕ ⟶ ℕ ⟶ bool  = [n,m] ∃! [x] n + x ≐ m  # 1  2 prec 105 
	geq : ℕ ⟶ ℕ ⟶ bool  = [n,m] m ≤ n  # 1  2 prec 105 
	lessthan : ℕ ⟶ ℕ ⟶ bool  = [n,m] n ≤ m ∧ n ≠ m  # 1 < 2 prec 105 
	morethan : ℕ ⟶ ℕ ⟶ bool  = [n,m] n ≥ m ∧ n ≠ m  # 1 > 2 prec 105 
	
	/T Others ❙
	max : ℕ ⟶ ℕ ⟶ ℕ  # max 1 2 
	min : ℕ ⟶ ℕ ⟶ ℕ  # min 1 2 
	
	mod : ℕ ⟶ ℕ ⟶ ℕ  # 1 mod 2 prec 25 
	// axiom_mod1: ⊦ ∀[n] ∀[m] n < m ⇒ (n mod m) ≐ n ❙
	// axiom_mod2: ⊦ ∀[n] ∀[m] (m ≤ n) ⇒ ((n mod m) ≐ ((n - m) mod m)) ❙

	primes : type  = ⟨ x : ℕ+ | ⊦ x ≠ 1 ∧ ∀ [y : ℕ] (y | x) ⇒ (y ≐ 1 ∨ y ≐ x) ⟩ 
	fromOneTo : ℕ+ ⟶ type  = [n] ⟨ x: ℕ+ | ⊦ 1 ≤ x ∧ x ≤ n ⟩ 
	
	/T Monoid Axioms ❙
	axiom_associativePlus : {x: ℕ,y,z} ⊦ x + (y + z) ≐ (x + y) + z  # associative_plus_nat 1 2 3
	axiom_leftUnitalPlus : {x : ℕ} ⊦ 0 + x ≐ x  # leftunital_plus_nat 
	lemma_rightUnitalPlus : {x : ℕ} ⊦ x + 0 ≐ x  = axiom_plus1  # rightunital_plus_nat