#m #n * -m -n /3 width=1 by yle_inj, monotonic_pred/
qed.
(* Properties on successor **************************************************)
#m #n * -m -n /3 width=1 by yle_inj, monotonic_pred/
qed.
(* Properties on successor **************************************************)