∀ {ι : Type u_3} {M : Type u_4} {N : Type u_1} [inst : AddCommGroup M] [inst_1 : AddCommGroup N] [Finite ι]
  {k : Type u_2} [inst_3 : Field k] [CharZero k] [inst_5 : Module k M] [inst_6 : Module k N] (p : M →ₗ[k] N →ₗ[k] k)
  [p.IsPerfPair] (root : ι ↪ M) (coroot : ι ↪ N),
  (∀ (i : ι), (p (root i)) (coroot i) = 2) →
    (∀ (i : ι), Set.MapsTo (⇑(Module.preReflection (root i) (p.flip (coroot i)))) (Set.range ⇑root) (Set.range ⇑root)) →
      Submodule.span k (Set.range ⇑root) = ⊤ →
        ∀ (i : ι), Set.MapsTo (⇑(Module.preReflection (coroot i) (p (root i)))) (Set.range ⇑coroot) (Set.range ⇑coroot)