Beginner: How to complete the induction case in a proof that all multiples are a product of the least common multiple

As a disclaimer, I'm fairly new to higher-level mathematics and this is my first question here, so please let me know if I need to clarify anything.

I am trying to prove that if I have some natural number $x$ that's a multiple of two other natural numbers $a$ and $b$, where $a$ and $b$ are coprime, then it's also a multiple of the least common denominator. Or, alternatively, for any $x$, there exists a $c \ge 1$ such that $abc=x$.

My basic strategy is to do a proof by induction on $a, b,$ and $x$. I am using the Coq proof assistant.

I have formulated it as follows:

$ (x \bmod a = 0) \land (x \bmod b = 0) \land (a \bmod b > 0) \land (b \bmod a > 0) \implies (x \bmod (a b)) = 0$

meaning that if some number $x$ is divisible by both $a$ and $b$` separately and $a$ and $b$ are coprime, then it's also divisible by the least common multiple of them.

I'm left with the following case to prove:

$ S x \bmod (S a * S b) = 0$

with the following premises:

$ a, b, x \in \mathbb{N} \\ H : S x \bmod S a = 0 \land S x \bmod S b = 0 \land S a \bmod S b > 0 \land S b \bmod S a > 0 \\ IHa : S x \bmod a = 0 \land S x \bmod S b = 0 \land a \bmod S b > 0 \land S b \bmod a > 0 \\ \qquad \implies S x \bmod (a * S b) = 0 \\ $

I'm hoping I'm not missing something really obvious here, but I'm a little confused about how to proceed at this point as this seems rather like a restatement of my original goal.

Again, this is my first post here, so please let me know if I need to edit.

Edit: I almost forgot, here's the proof I have so far in Coq:

Require Import Coq.Init.Nat.

(* Added for convenience - dumb name I know, but basically it says that 0 / x = 0 in every case *)
Axiom ZeroDividesAll : forall a,
    0 mod a = 0.

(* I'm trying to prove that everything is a multiple of the least common multiple *)
Theorem EverythingIsAMultipleOfLCM : forall a b x : nat,
(x mod a = 0) /\ (x mod b = 0) /\ (a mod b > 0) /\ (b mod a > 0) -> (x mod (a * b)) = 0.
Proof.
intros.
(* Obviously I'm doing a proof by induction *)
induction a, b, x.
reflexivity. (* 0 mod 0 = 0 *)
apply H. (* The next few cases follow immediately from the premises *)
apply H.
apply H.
rewrite <- mult_n_O. (* This case is 0 mod (a * 0) = 0 - use the fact that a * 0 = 0 first *)
reflexivity. (* Now we're left with 0 mod 0 = 0 *)
rewrite <- mult_n_O.
apply H. (* This also follows from the inductive hypothesis *)
apply ZeroDividesAll.
(* This is where I get stuck *)

Below is one simple way to conceptualize such proofs that proceed inductively by Euclidean descent. It should be possible to easily encode such proofs in any automated theorem prover.

That $\ a,b\mid m\,\Rightarrow\,{\rm lcm}(a,b)\mid m\ $ may be conceptually proved by Euclidean descent as below.

The set $M$ of all positive common multiples of all $\,a,b\,$ is closed under positive subtraction, i.e. $\,m> n\in M$ $\Rightarrow$ $\,a,b\mid m,n\,\Rightarrow\, a,b\mid m\!-\!n\,\Rightarrow\,m\!-\!n\in M.\,$ Therefore, by induction, we deduce that $\,M\,$ is also closed under mod, i.e. remainder, since it arises by repeated subtraction, i.e. $\ m\ {\rm mod}\ n\, =\, m-qn = ((m-n)-n)-\cdots-n.\,$ Thus the least $\,\ell\in M\,$ divides every $\,m\in M,\,$ else $\ 0\ne m\ {\rm mod}\ \ell\ $ lies in $\,M\,$ and is smaller than $\,\ell,\,$ contra minimality of $\,\ell.$

This immediately yields the following fundamental

Theorem $\,\ a,b\mid m\iff {\rm lcm}(a,b)\mid m\quad$ [Universal Property of LCM]

Proof $\ $ The direction $(\Rightarrow)$ was proved above. The converse $(\Leftarrow)$ follows by definition of lcm and transitivity of divisibility: $\ a,b\mid {\rm lcm}(a,b)\mid m\,$ $\Rightarrow$ $\,a,b\mid m.$

The above says that lcm is a divisibility-least common multiple, i.e. it is least in the divisibility order $\, a\prec b\!\! \overset{\rm def}\iff\! a\mid b.\ $ This is the (universal) definition of lcm used in general rings (which generally lack structure needed to measure "least"). See here for more on the general viewpoint.

Remark $\ $ The key algebraic structure exploited in the proof is abstracted out in the Lemma below.

Lemma $\ \ $ Let $\,\rm S\ne\emptyset \,$ be a set of integers $>0$ closed under subtraction $> 0,\,$ i.e. for all $\rm\,n,m\in S, \,$ $\rm\ n > m\ \Rightarrow\ n-m\, \in\, S.\,$ Then the least $\rm\:\ell\in S\,$ divides every element of $\,\rm S.$

Proof ${\bf\ 1}\,\ $ If not there is a least nonmultiple $\rm\,n\in S,\,$ contra $\rm\,n-\ell \in S\,$ is a nonmultiple of $\rm\,\ell.$

Proof ${\bf\ 2}\,\rm\,\ \ S\,$ closed under subtraction $\rm\,\Rightarrow\,S\,$ closed under remainder (mod), when it is $\ne 0,$ because mod is simply repeated subtraction, i.e. $\rm\, a\ mod\ b\, =\, a - k b\, =\, a-b-b-\cdots -b.\,$ Thus $\rm\,n\in S\,$ $\Rightarrow$ $\rm\, (n\ mod\ \ell) = 0,\,$ else it is $\rm\,\in S\,$ and smaller than $\rm\,\ell,\,$ contra minimality of $\rm\,\ell.$

In a nutshell, two applications of induction yield the following inferences

$ \rm\begin{eqnarray} S\ closed\ under\ {\bf subtraction} &\:\Rightarrow\:&\rm S\ closed\ under\ {\bf mod} = remainder = repeated\ subtraction \\ &\:\Rightarrow\:&\rm S\ closed\ under\ {\bf gcd} = repeated\ mod\ (Euclid's\ algorithm) \end{eqnarray}$

Interpreted constructively, this yields the extended Euclidean algorithm for the gcd.

That innate structure of the set of common multiples will be clarified when one studies ideal theory in abstract algebra, viz. the set of common multiples is a prototypical example of an ideal, and the above proof $2$ using descent by mod / remainder is a special case that ideals are principal in domains enjoying (Euclidean) Division with Remainder, i.e. Euclidean domains are PIDs. The proof is exactly the same as above, by Euclidean descent using the division algorithm.

An answer on your approach rather than the actual issue you're tackling: You seems to be trying to run induction on three different variables simultaneously, and that's not going to work unless those variables are directly defined to be at fixed spacing (in which case the induction would be on the generating variable, so still only on one variable really). You could potentially run induction on one of $a,b$ (and then argue the other side by symmetry, perhaps) but even that would be tricky given the coprime requirement. Otherwise you would have to run three (or perhaps two) induction proofs in succession.

Induction is not an obvious candidate for this proof, in my opinion, although people sometimes surprise me with what they can achieve in unlikely ways.

Also, a couple of specific observation:

• this statement: $$a \not\equiv 0 \bmod b \land b \not\equiv 0 \bmod a$$ is not the same as saying that $a$ and $b$ are coprime; $a=6, b=9$ is a counterexample.
• if $a$ and $b$ are coprime, the least common multiple is always $ab$. So actually you have two options: forget about the coprime requirement, and just talk about least common multiples, for a broader proof, or stay focussed on coprimality and then you can forget about the least common multiple.