∀ {R : Type u_2} [inst : Ring R] {E : Type u_1} [inst_1 : AddCommGroup E] [inst_2 : Module R E] (p q : Submodule R E),
  IsCompl p q → Function.Injective ⇑(p.subtype.coprod q.subtype) ∧ Function.Surjective ⇑(p.subtype.coprod q.subtype)