-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 le_times_l.assumption.
-apply le_times_r.assumption.
-qed.
+(*
+theorem le_times_l: \forall p,n,m:nat. n \le m \to n*p \le m*p
+\def monotonic_le_times_l. *)
+
+ntheorem le_times: ∀n1,n2,m1,m2:nat.
+n1 ≤ n2 → m1 ≤ m2 → n1*m1 ≤ n2*m2.
+#n1; #n2; #m1; #m2; #len; #lem;
+napply transitive_le; (* too slow *)
+ ##[ ##| napply monotonic_le_times_l;//;
+ ##| napply monotonic_le_times_r;//;
+ ##]
+nqed.