theorem monotonic_le_plus_l:
\forall m:nat.monotonic nat le (\lambda n.n + m).
simplify.intros.
-rewrite < sym_plus.rewrite < sym_plus m.
+rewrite < sym_plus.rewrite < (sym_plus m).
apply le_plus_r.assumption.
qed.
theorem le_plus: \forall n1,n2,m1,m2:nat. n1 \le n2 \to m1 \le m2
\to n1 + m1 \le n2 + m2.
intros.
-apply trans_le ? (n2 + m1).
+apply (trans_le ? (n2 + m1)).
apply le_plus_l.assumption.
apply le_plus_r.assumption.
qed.
theorem le_plus_n :\forall n,m:nat. m \le n + m.
-intros.change with O+m \le n+m.
+intros.change with (O+m \le n+m).
apply le_plus_l.apply le_O_n.
qed.
theorem monotonic_le_times_l:
\forall m:nat.monotonic nat le (\lambda n.n*m).
simplify.intros.
-rewrite < sym_times.rewrite < sym_times m.
+rewrite < sym_times.rewrite < (sym_times m).
apply le_times_r.assumption.
qed.
theorem le_times: \forall n1,n2,m1,m2:nat. n1 \le n2 \to m1 \le m2
\to n1*m1 \le n2*m2.
intros.
-apply trans_le ? (n2*m1).
+apply (trans_le ? (n2*m1)).
apply le_times_l.assumption.
apply le_times_r.assumption.
qed.
elim (plus_n_O ?).apply le_n.
simplify.rewrite < sym_plus.apply le_plus_n.
qed.
-