theorem monotonic_lt_plus_l:
\forall n:nat.monotonic nat lt (\lambda m.m+n).
-change with (\forall n,p,q:nat. p < q \to p + n < q + n).
+simplify.
intros.
rewrite < sym_plus. rewrite < (sym_plus n).
apply lt_plus_r.assumption.
rewrite > (sym_plus q).assumption.
qed.
+theorem le_to_lt_to_plus_lt: \forall a,b,c,d:nat.
+a \le c \to b \lt d \to (a + b) \lt (c+d).
+intros.
+cut (a \lt c \lor a = c)
+[ elim Hcut
+ [ apply (lt_plus );
+ assumption
+ | rewrite > H2.
+ apply (lt_plus_r c b d).
+ assumption
+ ]
+| apply le_to_or_lt_eq.
+ assumption
+]
+qed.
+
+
(* times and zero *)
theorem lt_O_times_S_S: \forall n,m:nat.O < (S n)*(S m).
intros.simplify.unfold lt.apply le_S_S.apply le_O_n.
qed.
+theorem lt_times_eq_O: \forall a,b:nat.
+O \lt a \to (a * b) = O \to b = O.
+intros.
+apply (nat_case1 b)
+[ intros.
+ reflexivity
+| intros.
+ rewrite > H2 in H1.
+ rewrite > (S_pred a) in H1
+ [ apply False_ind.
+ apply (eq_to_not_lt O ((S (pred a))*(S m)))
+ [ apply sym_eq.
+ assumption
+ | apply lt_O_times_S_S
+ ]
+ | assumption
+ ]
+]
+qed.
+
+theorem O_lt_times_to_O_lt: \forall a,c:nat.
+O \lt (a * c) \to O \lt a.
+intros.
+apply (nat_case1 a)
+[ intros.
+ rewrite > H1 in H.
+ simplify in H.
+ assumption
+| intros.
+ apply lt_O_S
+]
+qed.
+
(* times *)
theorem monotonic_lt_times_r:
\forall n:nat.monotonic nat lt (\lambda m.(S n)*m).
-change with (\forall n,p,q:nat. p < q \to (S n) * p < (S n) * q).
+simplify.
intros.elim n.
simplify.rewrite < plus_n_O.rewrite < plus_n_O.assumption.
-change with (p + (S n1) * p < q + (S n1) * q).
apply lt_plus.assumption.assumption.
qed.
+(* a simple variant of the previus monotionic_lt_times *)
+theorem monotonic_lt_times_variant: \forall c:nat.
+O \lt c \to monotonic nat lt (\lambda t.(t*c)).
+intros.
+apply (increasing_to_monotonic).
+unfold increasing.
+intros.
+simplify.
+rewrite > sym_plus.
+rewrite > plus_n_O in \vdash (? % ?).
+apply lt_plus_r.
+assumption.
+qed.
+
theorem lt_times_r: \forall n,p,q:nat. p < q \to (S n) * p < (S n) * q
\def monotonic_lt_times_r.
theorem monotonic_lt_times_l:
\forall m:nat.monotonic nat lt (\lambda n.n * (S m)).
-change with
-(\forall n,p,q:nat. p < q \to p*(S n) < q*(S n)).
+simplify.
intros.
-rewrite < sym_times.rewrite < (sym_times (S n)).
+rewrite < sym_times.rewrite < (sym_times (S m)).
apply lt_times_r.assumption.
qed.
apply (ltn_to_ltO p q H2).
qed.
+theorem lt_times_r1:
+\forall n,m,p. O < n \to m < p \to n*m < n*p.
+intros.
+elim H;apply lt_times_r;assumption.
+qed.
+
+theorem lt_times_l1:
+\forall n,m,p. O < n \to m < p \to m*n < p*n.
+intros.
+elim H;apply lt_times_l;assumption.
+qed.
+
+theorem lt_to_le_to_lt_times :
+\forall n,n1,m,m1. n < n1 \to m \le m1 \to O < m1 \to n*m < n1*m1.
+intros.
+apply (le_to_lt_to_lt ? (n*m1))
+ [apply le_times_r.assumption
+ |apply lt_times_l1
+ [assumption|assumption]
+ ]
+qed.
+
theorem lt_times_to_lt_l:
\forall n,p,q:nat. p*(S n) < q*(S n) \to p < q.
intros.
exact (decidable_lt p q).
qed.
+theorem lt_times_n_to_lt:
+\forall n,p,q:nat. O < n \to p*n < q*n \to p < q.
+intro.
+apply (nat_case n)
+ [intros.apply False_ind.apply (not_le_Sn_n ? H)
+ |intros 4.apply lt_times_to_lt_l
+ ]
+qed.
+
theorem lt_times_to_lt_r:
\forall n,p,q:nat. (S n)*p < (S n)*q \to lt p q.
intros.
assumption.
qed.
+theorem lt_times_n_to_lt_r:
+\forall n,p,q:nat. O < n \to n*p < n*q \to lt p q.
+intro.
+apply (nat_case n)
+ [intros.apply False_ind.apply (not_le_Sn_n ? H)
+ |intros 4.apply lt_times_to_lt_r
+ ]
+qed.
+
theorem nat_compare_times_l : \forall n,p,q:nat.
nat_compare p q = nat_compare ((S n) * p) ((S n) * q).
intros.apply nat_compare_elim.intro.
unfold lt. apply le_n.assumption.
qed.
+
(* general properties of functions *)
theorem monotonic_to_injective: \forall f:nat\to nat.
monotonic nat lt f \to injective nat nat f.