-This line, and those below, will be ignored--
M library/nat/ord.ma
M library/nat/gcd.ma
M library/nat/factorization.ma
M library/technicalities/setoids.ma
apply (trans_lt ? (S O));
[ unfold lt; apply le_n;
| assumption; ] *) ] ]
apply (trans_lt ? (S O));
[ unfold lt; apply le_n;
| assumption; ] *) ] ]
- | letin x \def prime. auto new.
(*
apply prime_to_nth_prime;
apply prime_smallest_factor_n;
(*
apply prime_to_nth_prime;
apply prime_smallest_factor_n;
cut (prime (nth_prime (max_prime_factor n))).
apply lt_O_nth_prime_n.apply prime_nth_prime.
cut (nth_prime (max_prime_factor n) \divides n).
cut (prime (nth_prime (max_prime_factor n))).
apply lt_O_nth_prime_n.apply prime_nth_prime.
cut (nth_prime (max_prime_factor n) \divides n).
(*
[ apply (transitive_divides ? n);
[ apply divides_max_prime_factor_n.
(*
[ apply (transitive_divides ? n);
[ apply divides_max_prime_factor_n.
theorem divides_mod: \forall p,m,n:nat. O < n \to p \divides m \to p \divides n \to
p \divides (m \mod n).
intros.elim H1.elim H2.
theorem divides_mod: \forall p,m,n:nat. O < n \to p \divides m \to p \divides n \to
p \divides (m \mod n).
intros.elim H1.elim H2.
-apply (witness ? ? (n2 - n1*(m / n))).
+(* apply (witness ? ? (n2 - n1*(m / n))). *)
+apply witness[|
rewrite > distr_times_minus.
rewrite > distr_times_minus.
+rewrite < H3 in \vdash (? ? ? (? % ?)).
-rewrite < H4.
-apply sym_eq.
-apply plus_to_minus.
+rewrite < H4 in \vdash (? ? ? (? ? (? % ?))).
+apply sym_eq.apply plus_to_minus.
-apply div_mod.
-assumption.
+letin x \def div.
+rewrite < (div_mod ? ? H).
+reflexivity.
+]
qed.
theorem divides_mod_to_divides: \forall p,m,n:nat. O < n \to
qed.
theorem divides_mod_to_divides: \forall p,m,n:nat. O < n \to
apply (absurd ? ? H10 H7).
(* rewrite > H6.
rewrite > H8. *)
apply (absurd ? ? H10 H7).
(* rewrite > H6.
rewrite > H8. *)
-auto paramodulation library=yes.
unfold prime in H. elim H. assumption.
qed.
unfold prime in H. elim H. assumption.
qed.
unfold transitive in H;
unfold symmetric in sym;
intro;
unfold transitive in H;
unfold symmetric in sym;
intro;