Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Assume H0: nat_p x0.
Let x1 of type ι be given.
Assume H1: nat_p x1.
Let x2 of type ι be given.
Assume H2: nat_p x2.
Apply unknownprop_dd5df7669a233e3d5e134397e0a0943dece6dcd81d988e2d3c963c02c7bcf901 with add_nat x0 x1, x2, λ x3 x4 . x4 = add_nat (mul_nat x0 x2) (mul_nat x1 x2) leaving 3 subgoals.
Apply unknownprop_3336121954edce0fefb5edee2ad1b426a9827aac09625122db0ff807b493dc73 with x0, x1 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
The subproof is completed by applying H2.
Apply unknownprop_dd5df7669a233e3d5e134397e0a0943dece6dcd81d988e2d3c963c02c7bcf901 with x0, x2, λ x3 x4 . mul_nat x2 (add_nat x0 x1) = add_nat x4 (mul_nat x1 x2) leaving 3 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H2.
Apply unknownprop_dd5df7669a233e3d5e134397e0a0943dece6dcd81d988e2d3c963c02c7bcf901 with x1, x2, λ x3 x4 . mul_nat x2 (add_nat x0 x1) = add_nat (mul_nat x2 x0) x4 leaving 3 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H2.
Apply unknownprop_7f023976a8daf041aa17d3220ad6430692e696ae1148f2cbd9b38476d90b1552 with x2, x0, x1 leaving 3 subgoals.
The subproof is completed by applying H2.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
■