(* a particular case of the previous theorem, with c=1 *)
theorem divides_d_gcd: ∀m,n,d.
(* a particular case of the previous theorem, with c=1 *)
theorem divides_d_gcd: ∀m,n,d.
<commutative_plus >distributive_times_plus_r
>(div_mod m n) in ⊢(? ? (? % ?) ?)
>associative_times <commutative_plus >distributive_times_plus
<commutative_plus >distributive_times_plus_r
>(div_mod m n) in ⊢(? ? (? % ?) ?)
>associative_times <commutative_plus >distributive_times_plus
|(* 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
|(* 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