Theorem Path.Homotopic.projLeft_prod

Modification history