| false \Rightarrow
match p with
[O \Rightarrow n
- |(S q) \Rightarrow gcd_aux q n (mod m n)]].
+ |(S q) \Rightarrow gcd_aux q n (m \mod n)]].
definition gcd : nat \to nat \to nat \def
\lambda n,m:nat.
| (S p) \Rightarrow gcd_aux (S p) n (S p) ]].
theorem divides_mod: \forall p,m,n:nat. O < n \to p \divides m \to p \divides n \to
-p \divides mod m n.
+p \divides (m \mod n).
intros.elim H1.elim H2.
-apply witness ? ? (n2 - n1*(div m n)).
+apply witness ? ? (n2 - n1*(m / n)).
rewrite > distr_times_minus.
rewrite < H3.
rewrite < assoc_times.
rewrite < H4.
apply sym_eq.
apply plus_to_minus.
-rewrite > div_mod m n in \vdash (? ? %).
rewrite > sym_times.
-apply eq_plus_to_le ? ? (mod m n).
-reflexivity.
+apply div_mod.
assumption.
-rewrite > sym_times.
-apply div_mod.assumption.
qed.
theorem divides_mod_to_divides: \forall p,m,n:nat. O < n \to
-p \divides mod m n \to p \divides n \to p \divides m.
+p \divides (m \mod n) \to p \divides n \to p \divides m.
intros.elim H1.elim H2.
-apply witness p m ((n1*(div m n))+n2).
+apply witness p m ((n1*(m / n))+n2).
rewrite > distr_times_plus.
rewrite < H3.
rewrite < assoc_times.
change with
(match divides_b n1 m with
[ true \Rightarrow n1
-| false \Rightarrow gcd_aux n n1 (mod m n1)]) \divides m \land
+| false \Rightarrow gcd_aux n n1 (m \mod n1)]) \divides m \land
(match divides_b n1 m with
[ true \Rightarrow n1
-| false \Rightarrow gcd_aux n n1 (mod m n1)]) \divides n1.
+| false \Rightarrow gcd_aux n n1 (m \mod 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
-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.
+gcd_aux n n1 (m \mod n1) \divides m \land
+gcd_aux n n1 (m \mod n1) \divides n1.
+cut gcd_aux n n1 (m \mod n1) \divides n1 \land
+gcd_aux n n1 (m \mod n1) \divides mod m n1.
elim Hcut1.
split.apply divides_mod_to_divides ? ? n1.
assumption.assumption.assumption.assumption.
apply H.
-cut O \lt mod m n1 \lor O = mod m n1.
+cut O \lt m \mod n1 \lor O = mod m n1.
elim Hcut1.assumption.
apply False_ind.apply H4.apply mod_O_to_divides.
assumption.apply sym_eq.assumption.
apply lt_mod_m_m.assumption.
apply le_S_S_to_le.
apply trans_le ? n1.
-change with mod m n1 < n1.
+change with m \mod n1 < n1.
apply lt_mod_m_m.assumption.assumption.
assumption.assumption.
apply decidable_divides n1 m.assumption.
| false \Rightarrow
match m with
[ O \Rightarrow n
- | (S p) \Rightarrow gcd_aux (S p) n (S p) ]] \divides m
+ | (S p) \Rightarrow gcd_aux (S p) n (S p) ] ] \divides m
\land
match leb n m with
[ true \Rightarrow
| false \Rightarrow
match m with
[ O \Rightarrow n
- | (S p) \Rightarrow gcd_aux (S p) n (S p) ]] \divides 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.
d \divides
(match divides_b n1 m with
[ true \Rightarrow n1
-| false \Rightarrow gcd_aux n n1 (mod m n1)]).
+| false \Rightarrow gcd_aux n n1 (m \mod n1)]).
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 d \divides gcd_aux n n1 (mod m n1).
+change with d \divides gcd_aux n n1 (m \mod n1).
apply H.
-cut O \lt mod m n1 \lor O = mod m n1.
+cut O \lt m \mod n1 \lor O = m \mod n1.
elim Hcut1.assumption.
absurd n1 \divides m.apply mod_O_to_divides.
assumption.apply sym_eq.assumption.assumption.
apply lt_mod_m_m.assumption.
apply le_S_S_to_le.
apply trans_le ? n1.
-change with mod m n1 < n1.
+change with m \mod n1 < n1.
apply lt_mod_m_m.assumption.assumption.
assumption.
apply divides_mod.assumption.assumption.assumption.
\exists a,b.
a*n1 - b*m = match divides_b n1 m with
[ true \Rightarrow n1
-| false \Rightarrow gcd_aux n n1 (mod m n1)]
+| false \Rightarrow gcd_aux n n1 (m \mod n1)]
\lor
b*m - a*n1 = match divides_b n1 m with
[ true \Rightarrow n1
-| false \Rightarrow gcd_aux n n1 (mod m n1)].
+| false \Rightarrow gcd_aux n n1 (m \mod n1)].
elim Hcut1.
rewrite > divides_to_divides_b_true.
simplify.
rewrite > not_divides_to_divides_b_false.
change with
\exists a,b.
-a*n1 - b*m = gcd_aux n n1 (mod m n1)
+a*n1 - b*m = gcd_aux n n1 (m \mod n1)
\lor
-b*m - a*n1 = gcd_aux n n1 (mod m n1).
+b*m - a*n1 = gcd_aux n n1 (m \mod n1).
cut
\exists a,b.
-a*(mod m n1) - b*n1= gcd_aux n n1 (mod m n1)
+a*(m \mod n1) - b*n1= gcd_aux n n1 (m \mod n1)
\lor
-b*n1 - a*(mod m n1) = gcd_aux n n1 (mod m n1).
+b*n1 - a*(m \mod n1) = gcd_aux n n1 (m \mod n1).
elim Hcut2.elim H5.elim H6.
(* first case *)
rewrite < H7.
-apply ex_intro ? ? (a1+a*(div m n1)).
+apply ex_intro ? ? (a1+a*(m / n1)).
apply ex_intro ? ? a.
right.
rewrite < sym_plus.
assumption.
(* second case *)
rewrite < H7.
-apply ex_intro ? ? (a1+a*(div m n1)).
+apply ex_intro ? ? (a1+a*(m / n1)).
apply ex_intro ? ? a.
left.
+(* clear Hcut2.clear H5.clear H6.clear H. *)
rewrite > sym_times.
rewrite > distr_times_plus.
rewrite > sym_times.
rewrite < minus_n_n.reflexivity.
apply le_n.
assumption.
-apply H n1 (mod m n1).
-cut O \lt mod m n1 \lor O = mod m n1.
+apply H n1 (m \mod n1).
+cut O \lt m \mod n1 \lor O = m \mod n1.
elim Hcut2.assumption.
absurd n1 \divides m.apply mod_O_to_divides.
assumption.
apply lt_mod_m_m.assumption.
apply le_S_S_to_le.
apply trans_le ? n1.
-change with mod m n1 < n1.
+change with m \mod n1 < n1.
apply lt_mod_m_m.
assumption.assumption.assumption.assumption.
apply decidable_divides n1 m.assumption.
theorem eq_minus_gcd:
\forall m,n.\exists a,b.a*n - b*m = (gcd n m) \lor b*m - a*n = (gcd n m).
intros.
-change with
-\exists a,b.
-a*n - b*m =
-match leb n m with
- [ true \Rightarrow
- match n with
- [ O \Rightarrow m
- | (S p) \Rightarrow gcd_aux (S p) m (S p) ]
- | false \Rightarrow
- match m with
- [ O \Rightarrow n
- | (S p) \Rightarrow gcd_aux (S p) n (S p) ]]
-\lor b*m - a*n =
-match leb n m with
- [ true \Rightarrow
- match n with
- [ O \Rightarrow m
- | (S p) \Rightarrow gcd_aux (S p) m (S p) ]
- | false \Rightarrow
- match m with
- [ O \Rightarrow n
- | (S p) \Rightarrow gcd_aux (S p) n (S p) ]].
+unfold gcd.
apply leb_elim n m.
apply nat_case1 n.
simplify.intros.