Prove: $\forall l \in \mathbb{Z}: \forall r \in \mathbb{R}: 0 \le r \lt 1 \Rightarrow\lfloor l+r\rfloor = l$
My attempt:
Let: $l \in \mathbb{Z}, r \in \mathbb{R}.$
Assume: $0 \le r \lt 1.$
$\lfloor l + r \rfloor \le \lfloor l \rfloor + \lfloor r \rfloor = \lfloor l \rfloor + 0$, since $0 \le r \lt 1$.
$\lfloor l \rfloor + 0 = l$, since $l \in \mathbb{Z}$
Is that correct? This is for a beginners' proofs course.
On
Let $x=l+r$. Since $r \ge 0$ we have $l \le l+r=x$ and, since $r<1$ we have $x=l+r<l+r+(1-r)=l+1$.
Now use the fact that: $$ \forall l \in \mathbb{Z} \qquad \lfloor x \rfloor=l \iff l\le x\lt l+1 $$ that can be easily proved by the definition:
$$ \lfloor x \rfloor= \mbox{Max}\{n\in \mathbb{Z}, n\le x \} $$
Correctness depends on the properties of $\;\lfloor \cdots \rfloor\;$ that you are allowed to use. Since you gave none, let me use the following definition: for every real $\;x, y\;$, $$ \tag{0} \lfloor x \rfloor = y \;\;\equiv\;\; 0 \le x - y \lt 1 \;\land\; y \in \mathbb Z $$
$ \newcommand{\calc}{\begin{align} \quad &} \newcommand{\op}[1]{\\ #1 \quad & \quad \unicode{x201c}} \newcommand{\hints}[1]{\mbox{#1} \\ \quad & \quad \phantom{\unicode{x201c}} } \newcommand{\hint}[1]{\mbox{#1} \unicode{x201d} \\ \quad & } \newcommand{\then}{\Rightarrow} \newcommand{\when}{\Leftarrow} \newcommand{\endcalc}{\end{align}} \newcommand{\ref}[1]{\text{(#1)}} $Now, for any real $\;l,r\;$, let's see if we can use this definition to simplify $\;\lfloor l + r \rfloor = l\;$: $$\calc \tag 1 \lfloor l + r \rfloor = l \op=\hint{definition $\ref 0$ with $\;x,y := l+r, l\;$} 0 \le l+r - l \lt 1 \;\land\; l \in \mathbb Z \op=\hint{arithmetic: simplify} \tag 2 0 \le r \lt 1 \;\land\; l \in \mathbb Z \endcalc$$ This immediately proves the original statement, which says that $\ref 2$ implies $\ref 1$.
Update. In the comments you now specified that, instead, your basic properties/assumptions are the following, for real $\;x\;$ and for $\;n \in \mathbb Z\;$: \begin{align} \tag{A1a} & \lfloor x \rfloor \in \mathbb Z \\ \tag{A1b} & \lfloor x \rfloor \le x \\ \tag{A1c} & n \le x \;\then\; n \le \lfloor x \rfloor \\ \tag{A2} & n \le x \land \langle \forall z : z \in \mathbb Z : z \le x \then z \le n \rangle \;\then\; n = \lfloor x \rfloor \end{align} (Apologies for switching to a slightly different notation, which I am more used to, and which I feel focuses on the essentials. See EWD1300 for more details.)
Now one way to prove the original statement, is to again start with the main part that we're to prove: $$\calc \lfloor l + r \rfloor = l \op\when\hints{using $\ref{A2}$ using $\;l \in \mathbb Z\;$} \hint{-- this seems the only assumption directly applicable} l \le l + r \;\land\; \langle \forall z : z \in \mathbb Z : z \le l + r \then z \le l \rangle \op=\hint{LHS: simplify by subtracting $\;l\;$; RHS: substitute $\;z := z + l\;$} 0 \le r \;\land\; \langle \forall z : z \in \mathbb Z : z + l \le l + r \then z + l \le l \rangle \op=\hint{RHS: simplify by subtracting $\;l\;$; contraposition} 0 \le r \;\land\; \langle \forall z : z \in \mathbb Z : z \gt 0 \then z \gt r \rangle \op=\hint{RHS: ordering} 0 \le r \;\land\; r < 1 \endcalc$$ Note that we did not need to use any part of assumption 1.
Now you should try to take the proof from your question, together with Jon Mark Perry's suggestion, and write it in the above format: this forces you to add an explicit justification for each step.
However, be warned that the property $\;\lfloor x + y \rfloor \;\le\; \lfloor x \rfloor + \lfloor y \rfloor\;$ does not hold in general for all real $\;x,y\;$: e.g., $\;\lfloor \tfrac 1 2 + \tfrac 1 2 \rfloor \;=\; 1 \;>\; 0 \;=\; \lfloor \tfrac 1 2 \rfloor + \lfloor \tfrac 1 2 \rfloor\;$. Instead property $\ref 5$ below does hold.
Also, note that you would only be allowed to use the following properties, if you can prove them from $\ref{A1a}$, $\ref{A1b}$, $\ref{A1c}$, and $\ref{A2}$, for real $\;x,y\;$ and $\;n \in \mathbb Z\;$: \begin{align} \tag{3} & \lfloor n \rfloor \;=\; n \\ \tag{4} & x \le y \;\then\; \lfloor x \rfloor \le \lfloor y \rfloor \\ \tag{5} & \lfloor x \rfloor + \lfloor y \rfloor \;\le\; \lfloor x + y \rfloor \\ \tag{6} & 0 \le x \lt 1 \;\then\; \lfloor x \rfloor = 0 \\ \end{align}