(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/library_auto/nat/le_arith".
+set "baseuri" "cic:/matita/library_autobatch/nat/le_arith".
include "auto/nat/times.ma".
include "auto/nat/orders.ma".
simplify.intros.
elim n;simplify
[ assumption
-| auto
+| autobatch
(*apply le_S_S.assumption*)
]
qed.
simplify.intros.
rewrite < sym_plus.
rewrite < (sym_plus m).
- auto.
+ autobatch.
qed.
*)
theorem le_plus_l: \forall p,n,m:nat. n \le m \to n + p \le m + p
theorem le_plus: \forall n1,n2,m1,m2:nat. n1 \le n2 \to m1 \le m2
\to n1 + m1 \le n2 + m2.
intros.
-auto.
+autobatch.
(*apply (trans_le ? (n2 + m1)).
apply le_plus_l.assumption.
apply le_plus_r.assumption.*)
theorem le_plus_n :\forall n,m:nat. m \le n + m.
intros.
change with (O+m \le n+m).
-auto.
+autobatch.
(*apply le_plus_l.
apply le_O_n.*)
qed.
intros.
rewrite > H.
rewrite < sym_plus.
-apply le_plus_n. (* a questo punto funziona anche: auto.*)
+apply le_plus_n. (* a questo punto funziona anche: autobatch.*)
qed.
(* times *)
\forall n:nat.monotonic nat le (\lambda m. n * m).
simplify.intros.elim n;simplify
[ apply le_O_n.
-| auto.
+| autobatch.
(*apply le_plus;
assumption. *) (* chiudo entrambi i goal attivi in questo modo*)
]
simplify.intros.
rewrite < sym_times.
rewrite < (sym_times m).
-auto.
+autobatch.
qed.
*)
theorem le_times: \forall n1,n2,m1,m2:nat. n1 \le n2 \to m1 \le m2
\to n1*m1 \le n2*m2.
intros.
-auto.
+autobatch.
(*apply (trans_le ? (n2*m1)).
apply le_times_l.assumption.
apply le_times_r.assumption.*)
theorem le_times_n: \forall n,m:nat.(S O) \le n \to m \le n*m.
intros.elim H;simplify
-[ auto
+[ autobatch
(*elim (plus_n_O ?).
apply le_n....*)
-| auto
+| autobatch
(*rewrite < sym_plus.
apply le_plus_n.*)
]