Exact expanded PA statement
forall c d a. a = c * d -> a * a = c * (d * a)Structural proof guide
A factorization of a transports its square without expanding either factor.
Direct prerequisites: mul_assoc. The authored body proceeds by equality transport (1).
Proof neighborhood
Direct dependencies
Direct dependents
Formal native tactic body
Dependencies are hypotheses of this body receipt. The focused endpoint audits separately check the complete empty-context certificates.