(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/nat/gcd_properties1".
-
include "nat/gcd.ma".
(* this file contains some important properites of gcd in N *)
intros.
elim (H2 ((gcd a b)))
[ apply (antisymmetric_divides (gcd a b) c)
- [ apply (witness (gcd a b) c n2).
+ [ apply (witness (gcd a b) c n1).
assumption
| apply divides_d_gcd;
assumption
]
| assumption
]
- | apply (witness ? ? n2).
+ | apply (witness ? ? n1).
apply (inj_times_r1 (gcd a b) Hcut1).
rewrite < assoc_times.
rewrite < sym_times in \vdash (? ? (? % ?) ?).
| intros.
elim H1.
elim H2.
- cut(b = (d*n2) + a)
- [ cut (b - (d*n2) = a)
+ cut(b = (d*n1) + a)
+ [ cut (b - (d*n1) = a)
[ rewrite > H4 in Hcut1.
- rewrite < (distr_times_minus d n n2) in Hcut1.
+ rewrite < (distr_times_minus d n n1) in Hcut1.
apply divides_d_gcd
[ assumption
- | apply (witness d a (n - n2)).
+ | apply (witness d a (n - n1)).
apply sym_eq.
assumption
]