theorem copcom (a b: nat): $ coprime a b <-> coprime b a $;
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | eqeq1 | gcd a b = gcd b a -> (gcd a b = 1 <-> gcd b a = 1) |
|
| 2 | 1 | conv coprime | gcd a b = gcd b a -> (coprime a b <-> coprime b a) |
| 3 | gcdcom | gcd a b = gcd b a |
|
| 4 | 2, 3 | ax_mp | coprime a b <-> coprime b a |