∀ {G : Type u_1} (motive : AddRightCancelSemigroup G → Prop) (h : AddRightCancelSemigroup G),
  (∀ (add : G → G → G) (add_assoc : ∀ (a b c : G), a + b + c = a + (b + c))
      (add_right_cancel : ∀ (a : G), IsAddRightRegular a),
      motive { add := add, add_assoc := add_assoc, add_right_cancel := add_right_cancel }) →
    motive h