]>
matita.cs.unibo.it Git - helm.git/blobdiff - matita/library_auto/auto/Z/times.ma
| apply lt_O_times_S_S
| apply lt_O_times_S_S
]
| apply lt_O_times_S_S
| apply lt_O_times_S_S
]
(*simplify.
unfold lt.
apply le_SO_minus.
(*simplify.
unfold lt.
apply le_SO_minus.