[GOAL]
α : Type u_1
inst✝¹ : Ring α
inst✝ : Nontrivial α
C : PositiveCone α
src✝¹ : Ring α := inst✝¹
src✝ : OrderedAddCommGroup α := OrderedAddCommGroup.mkOfPositiveCone C.toPositiveCone
h : 0 = 1
⊢ False
[PROOFSTEP]
simpa [← h, C.pos_iff] using C.one_pos
[GOAL]
α : Type u_1
inst✝¹ : Ring α
inst✝ : Nontrivial α
C : PositiveCone α
src✝¹ : Ring α := inst✝¹
src✝ : OrderedAddCommGroup α := OrderedAddCommGroup.mkOfPositiveCone C.toPositiveCone
⊢ 0 ≤ 1
[PROOFSTEP]
change C.nonneg (1 - 0)
[GOAL]
α : Type u_1
inst✝¹ : Ring α
inst✝ : Nontrivial α
C : PositiveCone α
src✝¹ : Ring α := inst✝¹
src✝ : OrderedAddCommGroup α := OrderedAddCommGroup.mkOfPositiveCone C.toPositiveCone
⊢ AddCommGroup.PositiveCone.nonneg C.toPositiveCone (1 - 0)
[PROOFSTEP]
convert C.one_nonneg
[GOAL]
case h.e'_4
α : Type u_1
inst✝¹ : Ring α
inst✝ : Nontrivial α
C : PositiveCone α
src✝¹ : Ring α := inst✝¹
src✝ : OrderedAddCommGroup α := OrderedAddCommGroup.mkOfPositiveCone C.toPositiveCone
⊢ 1 - 0 = 1
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝¹ : Ring α
inst✝ : Nontrivial α
C : PositiveCone α
src✝¹ : Ring α := inst✝¹
src✝ : OrderedAddCommGroup α := OrderedAddCommGroup.mkOfPositiveCone C.toPositiveCone
x y : α
xp : 0 < x
yp : 0 < y
⊢ 0 < x * y
[PROOFSTEP]
change
  C.pos
    (x * y - 0)
      -- porting note: used to be convert, but it relied on unfolding definitions
[GOAL]
α : Type u_1
inst✝¹ : Ring α
inst✝ : Nontrivial α
C : PositiveCone α
src✝¹ : Ring α := inst✝¹
src✝ : OrderedAddCommGroup α := OrderedAddCommGroup.mkOfPositiveCone C.toPositiveCone
x y : α
xp : 0 < x
yp : 0 < y
⊢ AddCommGroup.PositiveCone.pos C.toPositiveCone (x * y - 0)
[PROOFSTEP]
rw [sub_zero]
[GOAL]
α : Type u_1
inst✝¹ : Ring α
inst✝ : Nontrivial α
C : PositiveCone α
src✝¹ : Ring α := inst✝¹
src✝ : OrderedAddCommGroup α := OrderedAddCommGroup.mkOfPositiveCone C.toPositiveCone
x y : α
xp : 0 < x
yp : 0 < y
⊢ AddCommGroup.PositiveCone.pos C.toPositiveCone (x * y)
[PROOFSTEP]
exact C.mul_pos x y (by rwa [← sub_zero x]) (by rwa [← sub_zero y])
[GOAL]
α : Type u_1
inst✝¹ : Ring α
inst✝ : Nontrivial α
C : PositiveCone α
src✝¹ : Ring α := inst✝¹
src✝ : OrderedAddCommGroup α := OrderedAddCommGroup.mkOfPositiveCone C.toPositiveCone
x y : α
xp : 0 < x
yp : 0 < y
⊢ AddCommGroup.PositiveCone.pos C.toPositiveCone x
[PROOFSTEP]
rwa [← sub_zero x]
[GOAL]
α : Type u_1
inst✝¹ : Ring α
inst✝ : Nontrivial α
C : PositiveCone α
src✝¹ : Ring α := inst✝¹
src✝ : OrderedAddCommGroup α := OrderedAddCommGroup.mkOfPositiveCone C.toPositiveCone
x y : α
xp : 0 < x
yp : 0 < y
⊢ AddCommGroup.PositiveCone.pos C.toPositiveCone y
[PROOFSTEP]
rwa [← sub_zero y]
