Let a, b, c and d be given.
Assume H.
Apply H to the current goal.
Assume H.
Apply H to the current goal.
Assume Hca: divides_int c a.
Assume Hcb: divides_int c b.
Assume Hcg: ∀d', divides_int d' a → divides_int d' b → d' ≤ c.
Assume H.
Apply H to the current goal.
Assume H.
Apply H to the current goal.
Assume Hda: divides_int d a.
Assume Hdb: divides_int d b.
Assume Hdg: ∀d', divides_int d' a → divides_int d' b → d' ≤ d.
Apply Hca to the current goal.
Assume H _.
Apply H to the current goal.
Assume Hc: c ∈ int.
Assume _.
Apply Hda to the current goal.
Assume H _.
Apply H to the current goal.
Assume Hd: d ∈ int.
Assume _.
Apply SNoLe_antisym c d (int_SNo c Hc) (int_SNo d Hd) to the current goal.
We will prove c ≤ d.
Apply Hdg to the current goal.
We will prove divides_int c a.
An exact proof term for the current goal is Hca.
We will prove divides_int c b.
An exact proof term for the current goal is Hcb.
We will prove d ≤ c.
Apply Hcg to the current goal.
We will prove divides_int d a.
An exact proof term for the current goal is Hda.
We will prove divides_int d b.
An exact proof term for the current goal is Hdb.
∎