∀ {N : Type u_1} {G : Type u_2} [inst : AddGroup N] [inst_1 : AddGroup G] {E : Type u_3} [inst_2 : AddGroup E]
  {S : AddGroupExtension N E G} (σ : S.Section) (g₁ g₂ : G), ∃ n, σ (g₁ + g₂) = σ g₁ + σ g₂ + S.inl n