no goals
X : Type u_2
inst✝² : NormedAddCommGroup X
M : Type u_1
inst✝¹ : Ring M
inst✝ : Module M X
P : { P // IsLprojection X P }
⊢ ↑P * ↑(Pᶜ) = 0
rw [coe_compl, mul_sub, mul_one, P.prop.proj.eq, sub_self]