Is this proof of 7 > 6 correct? High-schooler here. I tried to prove that 7 > 6 because it's fun:
Try
Definitions
1D — $[a ≥ b] ↔ [a-(z) = b, z \in \mathbb{N}]$
2D — $[a ≥ b] ↔ [(a=b) \lor (a>b)]$
3D — $[a \neq b] ↔ ¬[a=b]$
Proof
Using the identity axiom ($a + 0 = a$), we know that:
1: $7 + 0 = 7$
2: $7 = 7$  Simplifying line 1 using itself ($7 + 0 = 7$)
3: $7 - (1) = 7 - (1)$  Subtracting both sides by $(1)$ (identity axiom)
4: $7 - (1) = 6$ Simplifying $7-(1)$ on the equation's right side
If we define the natural numbers using the Peano's Axioms, we can extract that $1 \in \mathbb{N}$ (means: 1 is a natural number):
5: $7 - (1) = 6, 1 \in \mathbb{N}$
Now we can use 1D on line 5:
6: $7 ≥ 6$
Using 2D on line 6:
7: $(7=6) \lor (7>6)$
In order to don't prove too many things, we'll assume that $7 \neq 6$, even if we know it's true:
8: $7 \neq 6$
Using 3D on line 8:
9: $¬[7 = 6]$
Using logic (if A or B is/are true, and we know that A is false, then B is true) on lines 7 and 9:
10: $7>6$
Quod erat demonstratum: $7>6$

The definition 1D was adapted from the second paragraph of the answer of the question “what is the proof for 0 being less than 1?” in https://www.quora.com/What-is-proof-for-0-being-less-than-1. I didn't understand the answer, but I used his/her definition for it.
The definition 2D I took from the own name and idea of $≥$: “lesser or greater than”.
The definition 3D is the same thing as 2D. If $a+b$ is “a is equal to c", and $a \neq b$ is "a is not equal to b", it looked like a good definition: $[a \neq b] ↔ ¬[a=b]$
Questions
For whom is going to answer, please:
Is the proof correct? If so, is there a way it could be better? If it's wrong, what is wrong?
By the way, did I use Q.E.D. (Quod erat demonstratum) correctly?
Thank you very much for reading this.
P.S.: I didn't say “high-schooler here” in the start to increase what I did. I did it to assure that people would understand that my maths background is high school, so they wouldn't use too complex explanations.
 A: I am very happy to see people are still looking into the foundation of mathematics, the axioms this beautiful science started with. To answer your question:
$1$. I am quite positive your proof is correct and very rigorous. (I will ask a specialist and come with a confirmation)
$2$. Your $1D$ is equivalent to:

$\forall x,y (x<y\Rightarrow\exists z(x+z=y))$ (Everything that happens here, happens over $\mathbb{N}$)

$2'$. Regarding the quora post, that guy used the following interpretation:

The Peano axioms can be derived from set theoretic constructions of the natural numbers and axioms of set theory such as the Zermelo-Fraenkel set theory. The standard construction of the naturals, due to John von Neumann, starts from a definition of $0$ as the empty set, $\varnothing$, and an operator $s$ on sets defined as: $$s(a)=a\cup\{a\}$$ The set of natural numbers, $\mathbb{N}$ is defined as the intersection of all sets closed under $s$ that contain the empty set. Each natural number is equal (as a set) to the set of natural numbers less than it. For example: $$3=s(2)=s(\{0,1\})=\{0,1\}\cup\{\{0,1\}\}=\{0,1,\{0,1\}\}=\{0,1,2\}$$ The set $\mathbb{N}$ together with $0$ and the successor function $s:\mathbb{N}\rightarrow\mathbb{N}$ satisfies the Peano axioms.

This is what he meant. $a<b$ if $s(a)\in s(b)$. As $s(0)=\varnothing$, then $s(o)\in s(1)$ so we are done.
$2''$. Read this to see more about the Peano axioms and very many interpretations (this is where $1D$ comes from and the set theroretic interpretation that guy used in his quora post)
$3$. You should use $\mathcal{Q}.\mathcal{E}.\mathcal{D}$ after the statement you prove:

"$7>6$, Quod Erat Demonstrandum" not "Quod Erat Demonstrandum: $7>6$"

There is no exact translation,but it is used (mainly at end of proofs) with the meaning: "this completes the proof", "as required", "as desired", "as expected", "hence proved", "ergo", or other similar statements..
