Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Let x1 of type ι be given.
Assume H0: nat_p x0.
Assume H1: nat_p x1.
Assume H2: x0x1.
Let x2 of type ι be given.
Assume H3: nat_p x2.
Apply mul_nat_com with x2, x0, λ x3 x4 . x4mul_nat x2 x1 leaving 3 subgoals.
The subproof is completed by applying H3.
The subproof is completed by applying H0.
Apply mul_nat_com with x2, x1, λ x3 x4 . mul_nat x0 x2x4 leaving 3 subgoals.
The subproof is completed by applying H3.
The subproof is completed by applying H1.
Apply unknownprop_d99b106d8c3aa5eb23e015bc5d27fe6284c8a3a86f85a0911e7d46761f04ef97 with x0, x1, x2 leaving 4 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
The subproof is completed by applying H2.
The subproof is completed by applying H3.