theorem le_gcd_times: \forall m,n,p:nat. O< p \to gcd m n \le gcd m (n*p).
intros.
-apply (nat_case n).reflexivity.
+apply (nat_case n).apply le_n.
intro.
apply divides_to_le.
apply lt_O_gcd.
elim H1.rewrite > H6.
(* applyS (witness n (n*(q*a-a1*n2)) (q*a-a1*n2))
reflexivity. *);
- applyS (witness n ? ? (refl_eq ? ?)).
+ applyS (witness n ? ? (refl_eq ? ?)) timeout=50.
(*
rewrite < (sym_times n).rewrite < assoc_times.
rewrite > (sym_times q).rewrite > assoc_times.