right_div_gcd_ne_zero

theorem right_div_gcd_ne_zero : ∀ {R : Type u_1} [inst : EuclideanDomain R] [inst_1 : GCDMonoid R] {p q : R}, q ≠ 0 → q / gcd p q ≠ 0

This theorem states that for any type `R` that is an instance of the `EuclideanDomain` and `GCDMonoid` typeclasses, and any elements `p` and `q` of `R`, if `q` is not equal to zero, then the result of dividing `q` by the greatest common divisor (gcd) of `p` and `q` is also not equal to zero. In other words, in a Euclidean Domain, the division of a non-zero element by its gcd with any other element will never yield zero.

More concisely: In a Euclidean Domain, the quotient of any non-zero element by its greatest common divisor with another element is a non-zero element.