# Additional instances for ordered commutative groups. #

theorem OrderDual.orderedAddCommGroup.proof_4 {α : Type u_1} (n : ) (a : αᵒᵈ) :
= -SubNegMonoid.zsmul (n.succ) a
theorem OrderDual.orderedAddCommGroup.proof_5 {α : Type u_1} (a : αᵒᵈ) :
-a + a = 0
theorem OrderDual.orderedAddCommGroup.proof_7 {α : Type u_1} (a : αᵒᵈ) (b : αᵒᵈ) :
a b∀ (c : αᵒᵈ), c + a c + b
instance OrderDual.orderedAddCommGroup {α : Type u_1} :
Equations
theorem OrderDual.orderedAddCommGroup.proof_6 {α : Type u_1} (a : αᵒᵈ) (b : αᵒᵈ) :
a + b = b + a
theorem OrderDual.orderedAddCommGroup.proof_1 {α : Type u_1} (a : αᵒᵈ) (b : αᵒᵈ) :
a - b = a + -b
instance OrderDual.orderedCommGroup {α : Type u_1} [] :
Equations
• OrderDual.orderedCommGroup = let __src := OrderDual.orderedCommMonoid; let __src_1 := OrderDual.instGroup;
theorem OrderDual.linearOrderedAddCommGroup.proof_1 {α : Type u_1} (a : αᵒᵈ) (b : αᵒᵈ) :
a b b a
theorem OrderDual.linearOrderedAddCommGroup.proof_3 {α : Type u_1} (a : αᵒᵈ) (b : αᵒᵈ) :
max a b = if a b then b else a
Equations
• One or more equations did not get rendered due to their size.
theorem OrderDual.linearOrderedAddCommGroup.proof_2 {α : Type u_1} (a : αᵒᵈ) (b : αᵒᵈ) :
min a b = if a b then a else b
Equations
• One or more equations did not get rendered due to their size.