(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/nat/gcd".
-
include "nat/primes.ma".
include "nat/lt_arith.ma".
theorem divides_gcd_nm: \forall n,m.
gcd n m \divides m \land gcd n m \divides n.
intros.
-(*CSC: simplify simplifies too much because of a redex in gcd *)
change with
(match leb n m with
[ true \Rightarrow
qed.
theorem symmetric_gcd: symmetric nat gcd.
-(*CSC: bug here: unfold symmetric does not work *)
change with
(\forall n,m:nat. gcd n m = gcd m n).
intros.
]
qed.
+(*
+theorem divides_to_divides_times1: \forall p,q,n. prime p \to prime q \to p \neq q \to
+divides p n \to divides q n \to divides (p*q) n.
+intros.elim H3.
+rewrite > H5 in H4.
+elim (divides_times_to_divides ? ? ? H1 H4)
+ [elim H.apply False_ind.
+ apply H2.apply sym_eq.apply H8
+ [assumption
+ |apply prime_to_lt_SO.assumption
+ ]
+ |elim H6.
+ apply (witness ? ? n1).
+ rewrite > assoc_times.
+ rewrite < H7.assumption
+ ]
+qed.
+*)
+
+theorem divides_to_divides_times: \forall p,q,n. prime p \to p \ndivides q \to
+divides p n \to divides q n \to divides (p*q) n.
+intros.elim H3.
+rewrite > H4 in H2.
+elim (divides_times_to_divides ? ? ? H H2)
+ [apply False_ind.apply H1.assumption
+ |elim H5.
+ apply (witness ? ? n1).
+ rewrite > sym_times in ⊢ (? ? ? (? % ?)).
+ rewrite > assoc_times.
+ rewrite < H6.assumption
+ ]
+qed.
\ No newline at end of file