-(* spostare *)
-theorem le_plus_to_le:
-\forall a,n,m. a + n \le a + m \to n \le m.
-intro.
-elim a
- [assumption
- |apply H.
- apply le_S_S_to_le.assumption
- ]
-qed.
-
-theorem le_times_to_le:
-\forall a,n,m. O < a \to a * n \le a * m \to n \le m.
-intro.
-apply nat_elim2;intros
- [apply le_O_n
- |apply False_ind.
- rewrite < times_n_O in H1.
- generalize in match H1.
- apply (lt_O_n_elim ? H).
- intros.
- simplify in H2.
- apply (le_to_not_lt ? ? H2).
- apply lt_O_S
- |apply le_S_S.
- apply H
- [assumption
- |rewrite < times_n_Sm in H2.
- rewrite < times_n_Sm in H2.
- apply (le_plus_to_le a).
- assumption
- ]
- ]
-qed.
-
-theorem le_exp_to_le:
-\forall a,n,m. S O < a \to exp a n \le exp a m \to n \le m.
-intro.
-apply nat_elim2;intros
- [apply le_O_n
- |apply False_ind.
- apply (le_to_not_lt ? ? H1).
- simplify.
- rewrite > times_n_SO.
- apply lt_to_le_to_lt_times
- [assumption
- |apply lt_O_exp.apply lt_to_le.assumption
- |apply lt_O_exp.apply lt_to_le.assumption
- ]
- |simplify in H2.
- apply le_S_S.
- apply H
- [assumption
- |apply (le_times_to_le a)
- [apply lt_to_le.assumption|assumption]
- ]
- ]
-qed.
-