\land
gcd_aux (S m1) m (S m1) \divides (S m1)).
apply divides_gcd_aux_mn.
-simplify.apply le_S_S.apply le_O_n.
+unfold lt.apply le_S_S.apply le_O_n.
assumption.apply le_n.
simplify.intro.
apply (nat_case1 m).
gcd_aux (S m1) n (S m1) \divides S m1).
elim Hcut.split.assumption.assumption.
apply divides_gcd_aux_mn.
-simplify.apply le_S_S.apply le_O_n.
-apply not_lt_to_le.simplify.intro.apply H.
+unfold lt.apply le_S_S.apply le_O_n.
+apply not_lt_to_le.unfold Not. unfold lt.intro.apply H.
rewrite > H1.apply (trans_le ? (S n)).
apply le_n_Sn.assumption.apply le_n.
qed.
intros.
change with (d \divides gcd_aux (S m1) m (S m1)).
apply divides_gcd_aux.
-simplify.apply le_S_S.apply le_O_n.assumption.apply le_n.assumption.
+unfold lt.apply le_S_S.apply le_O_n.assumption.apply le_n.assumption.
rewrite < H2.assumption.
apply (nat_case1 m).simplify.intros.assumption.
intros.
change with (d \divides gcd_aux (S m1) n (S m1)).
apply divides_gcd_aux.
-simplify.apply le_S_S.apply le_O_n.
+unfold lt.apply le_S_S.apply le_O_n.
apply lt_to_le.apply not_le_to_lt.assumption.apply le_n.assumption.
rewrite < H2.assumption.
qed.
a*(S m1) - b*m = (gcd_aux (S m1) m (S m1))
\lor b*m - a*(S m1) = (gcd_aux (S m1) m (S m1))).
apply eq_minus_gcd_aux.
-simplify. apply le_S_S.apply le_O_n.
+unfold lt. apply le_S_S.apply le_O_n.
assumption.apply le_n.
apply (nat_case1 m).
simplify.intros.
apply (ex_intro ? ? a).
left.assumption.
apply eq_minus_gcd_aux.
-simplify. apply le_S_S.apply le_O_n.
+unfold lt. apply le_S_S.apply le_O_n.
apply lt_to_le.apply not_le_to_lt.assumption.
apply le_n.
qed.
apply divides_gcd_nm.
qed.
+theorem lt_O_gcd:\forall m,n:nat. O < n \to O < gcd m n.
+intros.
+apply (nat_case1 (gcd m n)).
+intros.
+generalize in match (gcd_O_to_eq_O m n H1).
+intros.elim H2.
+rewrite < H4 in \vdash (? ? %).assumption.
+intros.unfold lt.apply le_S_S.apply le_O_n.
+qed.
+
theorem symmetric_gcd: symmetric nat gcd.
change with
(\forall n,m:nat. gcd n m = gcd m n).
variant sym_gcd: \forall n,m:nat. gcd n m = gcd m n \def
symmetric_gcd.
+theorem le_gcd_times: \forall m,n,p:nat. O< p \to gcd m n \le gcd m (n*p).
+intros.
+apply (nat_case n).reflexivity.
+intro.
+apply divides_to_le.
+apply lt_O_gcd.
+rewrite > (times_n_O O).
+apply lt_times.unfold lt.apply le_S_S.apply le_O_n.assumption.
+apply divides_d_gcd.
+apply (transitive_divides ? (S m1)).
+apply divides_gcd_m.
+apply (witness ? ? p).reflexivity.
+apply divides_gcd_n.
+qed.
+
+theorem gcd_times_SO_to_gcd_SO: \forall m,n,p:nat. O < n \to O < p \to
+gcd m (n*p) = (S O) \to gcd m n = (S O).
+intros.
+apply antisymmetric_le.
+rewrite < H2.
+apply le_gcd_times.assumption.
+change with (O < gcd m n).
+apply lt_O_gcd.assumption.
+qed.
+
+(* for the "converse" of the previous result see the end of this development *)
+
theorem gcd_SO_n: \forall n:nat. gcd (S O) n = (S O).
intro.
-apply antisym_le.apply divides_to_le.simplify.apply le_n.
+apply antisym_le.apply divides_to_le.unfold lt.apply le_n.
apply divides_gcd_n.
cut (O < gcd (S O) n \lor O = gcd (S O) n).
elim Hcut.assumption.
apply le_to_or_lt_eq.apply le_O_n.
qed.
-theorem divides_gcd_mod: \forall m,n:nat. O < n \to O < m \to
+theorem divides_gcd_mod: \forall m,n:nat. O < n \to
divides (gcd m n) (gcd n (m \mod n)).
intros.
apply divides_d_gcd.
apply divides_gcd_m.
qed.
-theorem divides_mod_gcd: \forall m,n:nat. O < n \to O < m \to
+theorem divides_mod_gcd: \forall m,n:nat. O < n \to
divides (gcd n (m \mod n)) (gcd m n) .
intros.
apply divides_d_gcd.
apply divides_gcd_n.
-apply divides_mod_to_divides ? ? n.
+apply (divides_mod_to_divides ? ? n).
assumption.
apply divides_gcd_m.
apply divides_gcd_n.
qed.
+theorem gcd_mod: \forall m,n:nat. O < n \to
+(gcd n (m \mod n)) = (gcd m n) .
+intros.
+apply antisymmetric_divides.
+apply divides_mod_gcd.assumption.
+apply divides_gcd_mod.assumption.
+qed.
+
(* gcd and primes *)
theorem prime_to_gcd_SO: \forall n,m:nat. prime n \to n \ndivides m \to
gcd n m = (S O).
-intros.simplify in H.change with (gcd n m = (S O)).
+intros.unfold prime in H.change with (gcd n m = (S O)).
elim H.
apply antisym_le.
apply not_lt_to_le.
apply eq_minus_gcd.
assumption.assumption.
apply (decidable_divides n p).
-apply (trans_lt ? (S O)).simplify.apply le_n.
-simplify in H.elim H. assumption.
+apply (trans_lt ? (S O)).unfold lt.apply le_n.
+unfold prime in H.elim H. assumption.
+qed.
+
+theorem eq_gcd_times_SO: \forall m,n,p:nat. O < n \to O < p \to
+gcd m n = (S O) \to gcd m p = (S O) \to gcd m (n*p) = (S O).
+intros.
+apply antisymmetric_le.
+apply not_lt_to_le.
+unfold Not.intro.
+cut (divides (smallest_factor (gcd m (n*p))) n \lor
+ divides (smallest_factor (gcd m (n*p))) p).
+elim Hcut.
+apply (not_le_Sn_n (S O)).
+change with ((S O) < (S O)).
+rewrite < H2 in \vdash (? ? %).
+apply (lt_to_le_to_lt ? (smallest_factor (gcd m (n*p)))).
+apply lt_SO_smallest_factor.assumption.
+apply divides_to_le.
+rewrite > H2.unfold lt.apply le_n.
+apply divides_d_gcd.assumption.
+apply (transitive_divides ? (gcd m (n*p))).
+apply divides_smallest_factor_n.
+apply (trans_lt ? (S O)). unfold lt. apply le_n. assumption.
+apply divides_gcd_n.
+apply (not_le_Sn_n (S O)).
+change with ((S O) < (S O)).
+rewrite < H3 in \vdash (? ? %).
+apply (lt_to_le_to_lt ? (smallest_factor (gcd m (n*p)))).
+apply lt_SO_smallest_factor.assumption.
+apply divides_to_le.
+rewrite > H3.unfold lt.apply le_n.
+apply divides_d_gcd.assumption.
+apply (transitive_divides ? (gcd m (n*p))).
+apply divides_smallest_factor_n.
+apply (trans_lt ? (S O)). unfold lt. apply le_n. assumption.
+apply divides_gcd_n.
+apply divides_times_to_divides.
+apply prime_smallest_factor_n.
+assumption.
+apply (transitive_divides ? (gcd m (n*p))).
+apply divides_smallest_factor_n.
+apply (trans_lt ? (S O)).unfold lt. apply le_n. assumption.
+apply divides_gcd_m.
+change with (O < gcd m (n*p)).
+apply lt_O_gcd.
+rewrite > (times_n_O O).
+apply lt_times.assumption.assumption.
qed.
projects / helm.git / blobdiff