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.
Apply Subq_tra with mul_nat x0 x0, mul_nat x0 x1, mul_nat x1 x1 leaving 2 subgoals.
Apply unknownprop_929864532141b40b768d022d9a5eb271b4e76fb202303c61c5984df8eb73ceb2 with x0, x1, x0 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 H0.
Apply unknownprop_d99b106d8c3aa5eb23e015bc5d27fe6284c8a3a86f85a0911e7d46761f04ef97 with x0, x1, x1 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 H1.