[ O \Rightarrow n
| (S p) \Rightarrow gcd_aux (S p) n (S p) ]].
-theorem divides_mod: \forall p,m,n:nat. O < n \to divides p m \to divides p n \to
-divides p (mod m n).
+theorem divides_mod: \forall p,m,n:nat. O < n \to p \divides m \to p \divides n \to
+p \divides mod m n.
intros.elim H1.elim H2.
apply witness ? ? (n2 - n1*(div m n)).
rewrite > distr_times_minus.
qed.
theorem divides_mod_to_divides: \forall p,m,n:nat. O < n \to
-divides p (mod m n) \to divides p n \to divides p m.
+p \divides mod m n \to p \divides n \to p \divides m.
intros.elim H1.elim H2.
apply witness p m ((n1*(div m n))+n2).
rewrite > distr_times_plus.
qed.
theorem divides_gcd_aux_mn: \forall p,m,n. O < n \to n \le m \to n \le p \to
-divides (gcd_aux p m n) m \land divides (gcd_aux p m n) n.
+gcd_aux p m n \divides m \land gcd_aux p m n \divides n.
intro.elim p.
absurd O < n.assumption.apply le_to_not_lt.assumption.
-cut (divides n1 m) \lor \not (divides n1 m).
+cut (n1 \divides m) \lor (n1 \ndivides m).
change with
-(divides
(match divides_b n1 m with
[ true \Rightarrow n1
-| false \Rightarrow gcd_aux n n1 (mod m n1)]) m) \land
-(divides
+| false \Rightarrow gcd_aux n n1 (mod m n1)]) \divides m \land
(match divides_b n1 m with
[ true \Rightarrow n1
-| false \Rightarrow gcd_aux n n1 (mod m n1)]) n1).
+| false \Rightarrow gcd_aux n n1 (mod m n1)]) \divides n1.
elim Hcut.rewrite > divides_to_divides_b_true.
simplify.
split.assumption.apply witness n1 n1 (S O).apply times_n_SO.
assumption.assumption.
rewrite > not_divides_to_divides_b_false.
change with
-(divides (gcd_aux n n1 (mod m n1)) m) \land
-(divides (gcd_aux n n1 (mod m n1)) n1).
-cut (divides (gcd_aux n n1 (mod m n1)) n1) \land
-(divides (gcd_aux n n1 (mod m n1)) (mod m n1)).
+gcd_aux n n1 (mod m n1) \divides m \land
+gcd_aux n n1 (mod m n1) \divides n1.
+cut gcd_aux n n1 (mod m n1) \divides n1 \land
+gcd_aux n n1 (mod m n1) \divides mod m n1.
elim Hcut1.
split.apply divides_mod_to_divides ? ? n1.
assumption.assumption.assumption.assumption.
qed.
theorem divides_gcd_nm: \forall n,m.
-divides (gcd n m) m \land divides (gcd n m) n.
+gcd n m \divides m \land gcd n m \divides n.
intros.
change with
-divides
-(match leb n m with
+match leb n m with
[ true \Rightarrow
match n with
[ O \Rightarrow m
| false \Rightarrow
match m with
[ O \Rightarrow n
- | (S p) \Rightarrow gcd_aux (S p) n (S p) ]]) m
+ | (S p) \Rightarrow gcd_aux (S p) n (S p) ]] \divides m
\land
- divides
-(match leb n m with
+match leb n m with
[ true \Rightarrow
match n with
[ O \Rightarrow m
| false \Rightarrow
match m with
[ O \Rightarrow n
- | (S p) \Rightarrow gcd_aux (S p) n (S p) ]]) n.
+ | (S p) \Rightarrow gcd_aux (S p) n (S p) ]] \divides n.
apply leb_elim n m.
apply nat_case1 n.
simplify.intros.split.
apply witness m m (S O).apply times_n_SO.
apply witness m O O.apply times_n_O.
intros.change with
-divides (gcd_aux (S m1) m (S m1)) m
+gcd_aux (S m1) m (S m1) \divides m
\land
-divides (gcd_aux (S m1) m (S m1)) (S m1).
+gcd_aux (S m1) m (S m1) \divides (S m1).
apply divides_gcd_aux_mn.
simplify.apply le_S_S.apply le_O_n.
assumption.apply le_n.
apply witness n O O.apply times_n_O.
apply witness n n (S O).apply times_n_SO.
intros.change with
-divides (gcd_aux (S m1) n (S m1)) (S m1)
+gcd_aux (S m1) n (S m1) \divides (S m1)
\land
-divides (gcd_aux (S m1) n (S m1)) n.
-cut divides (gcd_aux (S m1) n (S m1)) n
+gcd_aux (S m1) n (S m1) \divides n.
+cut gcd_aux (S m1) n (S m1) \divides n
\land
-divides (gcd_aux (S m1) n (S m1)) (S m1).
+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 le_n_Sn.assumption.apply le_n.
qed.
-theorem divides_gcd_n: \forall n,m.
-divides (gcd n m) n.
+theorem divides_gcd_n: \forall n,m. gcd n m \divides n.
intros.
exact proj2 ? ? (divides_gcd_nm n m).
qed.
-theorem divides_gcd_m: \forall n,m.
-divides (gcd n m) m.
+theorem divides_gcd_m: \forall n,m. gcd n m \divides m.
intros.
exact proj1 ? ? (divides_gcd_nm n m).
qed.
theorem divides_gcd_aux: \forall p,m,n,d. O < n \to n \le m \to n \le p \to
-divides d m \to divides d n \to divides d (gcd_aux p m n).
+d \divides m \to d \divides n \to d \divides gcd_aux p m n.
intro.elim p.
absurd O < n.assumption.apply le_to_not_lt.assumption.
change with
-divides d
+d \divides
(match divides_b n1 m with
[ true \Rightarrow n1
| false \Rightarrow gcd_aux n n1 (mod m n1)]).
-cut divides n1 m \lor \not (divides n1 m).
+cut n1 \divides m \lor n1 \ndivides m.
elim Hcut.
rewrite > divides_to_divides_b_true.
simplify.assumption.
assumption.assumption.
rewrite > not_divides_to_divides_b_false.
-change with divides d (gcd_aux n n1 (mod m n1)).
+change with d \divides gcd_aux n n1 (mod m n1).
apply H.
cut O \lt mod m n1 \lor O = mod m n1.
elim Hcut1.assumption.
-absurd divides n1 m.apply mod_O_to_divides.
+absurd n1 \divides m.apply mod_O_to_divides.
assumption.apply sym_eq.assumption.assumption.
apply le_to_or_lt_eq.apply le_O_n.
apply lt_to_le.
qed.
theorem divides_d_gcd: \forall m,n,d.
-divides d m \to divides d n \to divides d (gcd n m).
+d \divides m \to d \divides n \to d \divides gcd n m.
intros.
change with
-divides d (
+d \divides
match leb n m with
[ true \Rightarrow
match n with
| false \Rightarrow
match m with
[ O \Rightarrow n
- | (S p) \Rightarrow gcd_aux (S p) n (S p) ]]).
+ | (S p) \Rightarrow gcd_aux (S p) n (S p) ]].
apply leb_elim n m.
apply nat_case1 n.simplify.intros.assumption.
intros.
-change with divides d (gcd_aux (S m1) m (S m1)).
+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.
rewrite < H2.assumption.
apply nat_case1 m.simplify.intros.assumption.
intros.
-change with divides d (gcd_aux (S m1) n (S m1)).
+change with d \divides gcd_aux (S m1) n (S m1).
apply divides_gcd_aux.
simplify.apply le_S_S.apply le_O_n.
apply lt_to_le.apply not_le_to_lt.assumption.apply le_n.assumption.
elim p.
absurd O < n.assumption.apply le_to_not_lt.assumption.
cut O < m.
-cut (divides n1 m) \lor \not (divides n1 m).
+cut n1 \divides m \lor n1 \ndivides m.
change with
\exists a,b.
a*n1 - b*m = match divides_b n1 m with
apply H n1 (mod m n1).
cut O \lt mod m n1 \lor O = mod m n1.
elim Hcut2.assumption.
-absurd divides n1 m.apply mod_O_to_divides.
+absurd n1 \divides m.apply mod_O_to_divides.
assumption.
symmetry.assumption.assumption.
apply le_to_or_lt_eq.apply le_O_n.
theorem gcd_O_to_eq_O:\forall m,n:nat. (gcd m n) = O \to
m = O \land n = O.
-intros.cut divides O n \land divides O m.
+intros.cut O \divides n \land O \divides m.
elim Hcut.elim H2.split.
assumption.elim H1.assumption.
rewrite < H.
apply le_to_or_lt_eq.apply le_O_n.
qed.
-theorem prime_to_gcd_SO: \forall n,m:nat. prime n \to \not (divides n m) \to
+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).
elim H.
apply le_to_or_lt_eq.apply le_O_n.
qed.
-theorem divides_times_to_divides: \forall n,p,q:nat.prime n \to divides n (p*q) \to
-divides n p \lor divides n q.
+theorem divides_times_to_divides: \forall n,p,q:nat.prime n \to n \divides p*q \to
+n \divides p \lor n \divides q.
intros.
-cut divides n p \lor \not (divides n p).
+cut n \divides p \lor n \ndivides p.
elim Hcut.
left.assumption.
right.
projects / helm.git / blobdiff