lemma divides_to_gcd_aux: ∀p,m,n. O < p → O < n →n ∣ m →
gcd_aux p m n = n.
-#p #m #n #posp @(lt_O_n_elim … posp) #l #posn #divnm normalize
+#p #m #n #posp @(lt_O_n_elim … posp) #l #posn #divnm whd in ⊢ (??%?)
>divides_to_dividesb_true normalize //
qed.
lemma not_divides_to_gcd_aux: ∀p,m,n. 0 < n → n ∤ m →
gcd_aux (S p) m n = gcd_aux p n (m \mod n).
-#p #m #n #lenm #divnm normalize >not_divides_to_dividesb_false
+#p #m #n #lenm #divnm whd in ⊢ (??%?) >not_divides_to_dividesb_false
normalize // qed.
theorem divides_gcd_aux_mn: ∀p,m,n. O < n → n ≤ m → n ≤ p →
(* a particular case of the previous theorem, with c=1 *)
theorem divides_d_gcd: ∀m,n,d.
- d ∣ m → d ∣ n → d ∣ gcd n m.
-/2/ (* bello *)
+ d ∣ m → d ∣ n → d ∣ gcd n m.
+#m #n #d #divdn #divdn applyS (divides_d_times_gcd m n d 1) //
qed.
theorem eq_minus_gcd_aux: ∀p,m,n.O < n → n ≤ m → n ≤ p →
<commutative_plus >distributive_times_plus_r
>(div_mod m n) in ⊢(? ? (? % ?) ?)
>associative_times <commutative_plus >distributive_times_plus
- <minus_minus <commutative_plus <plus_minus //
+ <minus_plus <commutative_plus <plus_minus //
|(* second case *)
<H @(ex_intro ?? (b+a*(m / n))) @(ex_intro ?? a) %1
>distributive_times_plus_r
>(div_mod m n) in ⊢ (? ? (? ? %) ?)
>distributive_times_plus >associative_times
- <minus_minus <commutative_plus <plus_minus //
+ <minus_plus <commutative_plus <plus_minus //
]
]
]