import GameServer.Commands

LemmaDoc MyNat.add_zero as "add_zero" in "Add"
"`add_zero (a : ℕ) : a + 0 = a`

This is one of the two axioms defining addition on `ℕ`."

LemmaDoc MyNat.add_succ as "add_succ" in "Add"
"`add_succ (a d : ℕ) : a + (succ d) = succ (a + d)`

This is the second axiom definiting addition on `ℕ`"

LemmaDoc MyNat.zero_add as "zero_add" in "Add"
"(missing)"

LemmaDoc MyNat.add_assoc as "add_assoc" in "Add"
"(missing)"

LemmaDoc MyNat.succ_add as "succ_add" in "Add"
"(missing)"

LemmaDoc MyNat.add_comm as "add_comm" in "Add"
"(missing)"

LemmaDoc MyNat.one_eq_succ_zero as "one_eq_succ_zero" in "Nat"
"(missing)"

LemmaDoc MyNat.succ_eq_add_one as "succ_eq_add_one" in "Add"
"(missing)"

LemmaDoc MyNat.add_one_eq_succ as "add_one_eq_succ" in "Add"
"(missing)"

LemmaDoc MyNat.add_right_comm as "add_right_comm" in "Add"
"(missing)"

LemmaDoc MyNat.succ_inj as "succ_inj" in "Nat"
"(missing)"

LemmaDoc MyNat.zero_ne_succ as "zero_ne_succ" in "Nat"
"(missing)"


/-? Multiplication World -/

LemmaDoc MyNat.mul_zero as "mul_zero" in "Mul"
"(missing)"

LemmaDoc MyNat.mul_succ as "mul_succ" in "Mul"
"(missing)"

LemmaDoc MyNat.zero_mul as "zero_mul" in "Mul"
"(missing)"

LemmaDoc MyNat.mul_one as "mul_one" in "Mul"
"(missing)"

LemmaDoc MyNat.one_mul as "one_mul" in "Mul"
"(missing)"

LemmaDoc MyNat.mul_add as "mul_add" in "Mul"
"(missing)"

LemmaDoc MyNat.mul_assoc as "mul_assoc" in "Mul"
"(missing)"

LemmaDoc MyNat.succ_mul as "succ_mul" in "Mul"
"(missing)"

LemmaDoc MyNat.add_mul as "add_mul" in "Mul"
"(missing)"

LemmaDoc MyNat.mul_comm as "mul_comm" in "Mul"
"(missing)"

LemmaDoc MyNat.mul_left_comm as "mul_left_comm" in "Mul"
"(missing)"



LemmaDoc MyNat.succ_eq_succ_of_eq as "succ_eq_succ_of_eq" in "Nat"
"(missing)"

LemmaDoc MyNat.add_right_cancel as "add_right_cancel" in "Add"
"(missing)"

LemmaDoc MyNat.add_left_cancel as "add_left_cancel" in "Add"
"(missing)"

LemmaDoc Ne.symm as "Ne.symm" in "Nat"
"(missing)"

LemmaDoc Eq.symm as "Eq.symm" in "Nat"
"(missing)"

LemmaDoc Iff.symm as "Iff.symm" in "Nat"
"(missing)"

LemmaDoc MyNat.succ_ne_zero as "succ_ne_zero" in "Add"
"(missing)"
  
LemmaDoc MyNat.add_right_cancel_iff as "add_right_cancel_iff" in "Add"
"(missing)"

LemmaDoc MyNat.eq_zero_of_add_right_eq_self as "eq_zero_of_add_right_eq_self" in "Add"
"(missing)"

LemmaDoc MyNat.add_left_eq_zero as "add_left_eq_zero" in "Add"
"(missing)"

LemmaDoc MyNat.add_right_eq_zero as "add_right_eq_zero" in "Add"
"(missing)"

LemmaDoc MyNat.eq_zero_or_eq_zero_of_mul_eq_zero as "eq_zero_or_eq_zero_of_mul_eq_zero" in "Mul"
"(missing)"

LemmaDoc MyNat.mul_left_cancel as "mul_left_cancel" in "Mul"
"(missing)"


LemmaDoc MyNat.zero_pow_zero as "zero_pow_zero" in "Pow"
"(missing)"

LemmaDoc MyNat.pow_zero as "pow_zero" in "Pow"
"(missing)"

LemmaDoc MyNat.pow_succ as "pow_succ" in "Pow"
"(missing)"

LemmaDoc MyNat.zero_pow_succ as "zero_pow_succ" in "Pow"
"(missing)"

LemmaDoc MyNat.pow_one as "pow_one" in "Pow"
"(missing)"

LemmaDoc MyNat.one_pow as "one_pow" in "Pow"
"(missing)"

LemmaDoc MyNat.pow_add as "pow_add" in "Pow"
"(missing)"

LemmaDoc MyNat.mul_pow as "mul_pow" in "Pow"
"(missing)"

LemmaDoc MyNat.pow_pow as "pow_pow" in "Pow"
"(missing)"

LemmaDoc MyNat.two_eq_succ_one as "two_eq_succ_one" in "Pow"
"(missing)"

LemmaDoc MyNat.add_squared as "add_squared" in "Pow"
"(missing)"

-- LemmaDoc MyNat. as "" in "Pow"
-- "(missing)"

-- LemmaDoc MyNat. as "" in "Pow"
-- "(missing)"

-- LemmaDoc MyNat. as "" in "Pow"
-- "(missing)"

-- LemmaDoc MyNat. as "" in "Pow"
-- "(missing)"

-- LemmaDoc MyNat. as "" in "Pow"
-- "(missing)"

