∀ {G : Type u_1} [inst : AddGroup G] {N : Type u_5} [inst_1 : AddGroup N],
  Relator.LiftFun (fun x1 x2 => x1 ≤ x2) (Relator.LiftFun (fun x1 x2 => x1 ≤ x2) fun x1 x2 => x1 ≤ x2) AddSubgroup.prod
    AddSubgroup.prod