Proofgold Proof

pf

Let x0 of type ι be given.

Let x1 of type ι be given.

Let x2 of type ι be given.

Let x3 of type ι be given.

Assume H0: divides_int x0 x1.

Assume H1: divides_int x0 x2.

Assume H2: divides_int x0 x3.

Apply divides_int_add_SNo with x0, x1, add_SNo x2 x3 leaving 2 subgoals.

The subproof is completed by applying H0.

Apply divides_int_add_SNo with x0, x2, x3 leaving 2 subgoals.

The subproof is completed by applying H1.

The subproof is completed by applying H2.

■