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).
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).
>associative_times <commutative_plus >distributive_times_plus
<minus_plus <commutative_plus <plus_minus //
|(* second case *)
<H @(ex_intro ?? (b+a*(m / n))) @(ex_intro ?? a) %1
>distributive_times_plus_r
>associative_times <commutative_plus >distributive_times_plus
<minus_plus <commutative_plus <plus_minus //
|(* second case *)
<H @(ex_intro ?? (b+a*(m / n))) @(ex_intro ?? a) %1
>distributive_times_plus_r
theorem gcd_1_to_divides_times_to_divides: ∀p,n,m:nat. O < p →
gcd p n = 1 → p ∣ (n*m) → p ∣ m.
#p #m #n #posn #gcd1 * #c #nm
theorem gcd_1_to_divides_times_to_divides: ∀p,n,m:nat. O < p →
gcd p n = 1 → p ∣ (n*m) → p ∣ m.
#p #m #n #posn #gcd1 * #c #nm
[@(quotient ?? (a*n-c*b)) >distributive_times_minus <associative_times
<associative_times <nm >(commutative_times m) >commutative_times
>associative_times <distributive_times_minus //
[@(quotient ?? (a*n-c*b)) >distributive_times_minus <associative_times
<associative_times <nm >(commutative_times m) >commutative_times
>associative_times <distributive_times_minus //
#divpn cases(divides_times_to_divides ??? primep divpn) #H
[@False_ind /2/
|cases H #c #eqb @(quotient ?? c) >eqb <associative_times //
#divpn cases(divides_times_to_divides ??? primep divpn) #H
[@False_ind /2/
|cases H #c #eqb @(quotient ?? c) >eqb <associative_times //