# Products of ordered commutative groups. #

theorem Prod.instOrderedAddCommGroup.proof_1 {G : Type u_1} {H : Type u_2} (a : G × H) (b : G × H) :
a b∀ (c : G × H), c + a c + b
instance Prod.instOrderedAddCommGroup {G : Type u_2} {H : Type u_3} :
Equations
instance Prod.instOrderedCommGroup {G : Type u_2} {H : Type u_3} [] [] :
Equations
• Prod.instOrderedCommGroup = let __src := Prod.instCommGroup; let __src_1 := ; let __src_2 := Prod.instOrderedCancelCommMonoid;
theorem Prod.Lex.orderedAddCommGroup.proof_1 {G : Type u_2} {H : Type u_1} :
∀ (x x_1 : Lex (G × H)), x x_1∀ (a : Lex (G × H)), a + x a + x_1
instance Prod.Lex.orderedAddCommGroup {G : Type u_2} {H : Type u_3} :
Equations
instance Prod.Lex.orderedCommGroup {G : Type u_2} {H : Type u_3} [] [] :
Equations
• Prod.Lex.orderedCommGroup =
theorem Prod.Lex.linearOrderedAddCommGroup.proof_3 {G : Type u_2} {H : Type u_1} (a : Lex (G × H)) (b : Lex (G × H)) :
min a b = if a b then a else b
theorem Prod.Lex.linearOrderedAddCommGroup.proof_2 {G : Type u_2} {H : Type u_1} (a : Lex (G × H)) (b : Lex (G × H)) :
a b b a
Equations