Proofgold Proof

pf
Apply mul_nat_SR with u6, u1, λ x0 x1 . x1 = u12 leaving 2 subgoals. The subproof is completed by applying nat_1. Apply mul_nat_1R with u6, λ x0 x1 . add_nat u6 x1 = u12. The subproof is completed by applying unknownprop_1405da4ddbfe657be591ff3f60e81b00e85c15d650392cce4bd374f2be095ac2. ■