[apply (bool_elim ? (leb ((S n1)*(S n1)) m))
[intro;rewrite > true_to_pi_p_Sn in \vdash (? ? ? (? % ?))
[rewrite > false_to_pi_p_Sn in \vdash (? ? ? (? ? %))
- [rewrite > H1;rewrite > H2;rewrite < assoc_times;reflexivity
+ [rewrite > H1;rewrite < assoc_times;reflexivity
|rewrite > H;lapply (leb_true_to_le ? ? H2);
lapply (le_to_not_lt ? ? Hletin);
apply (bool_elim ? (leb (S m) (S n1 * S n1)))
|rewrite > andb_sym;apply le_O_n]
|apply sigma_p_log_div;assumption]]]]
qed.
+(*
lemma le_prim_n_stima : \forall n,b. S O < b \to b \leq n \to
prim n \leq (S (((S (S (S (S O))))*(S (log b (pred n)))) +
|assumption]]
qed.
-lemma eq_div_div_times : \forall x,y,z.O < z \to O < y \to x/y = (z*x)/(z*y).
-intros.rewrite > (div_mod x y) in \vdash (? ? ? %);
- [rewrite > distr_times_plus;rewrite > sym_times;rewrite > assoc_times;
- rewrite > sym_times in ⊢ (? ? ? (? (? (? ? %) ?) ?));
- rewrite > div_plus_times
- [reflexivity
- |generalize in match H;cases z;intros
- [elim (not_le_Sn_O ? H2)
- |apply lt_times_r;apply lt_mod_m_m;assumption]]
- |assumption]
-qed.
-
alias num (instance 0) = "natural number".
lemma le_sigma_p_lemma1 : \forall n,b. S O < b \to b*b < n \to
(sigma_p n (\lambda x.leb (S n) (x*x))
|apply (trans_le ? ? ? ? H);apply lt_O_S]]]]]
apply (trans_le ? ? ? ? Hcut);
*)
+*)
\ No newline at end of file