no goals
α : Type u
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a : α
⊢ a⁺ ⊓ a⁻ = 1
rw [← mul_right_inj (a⁻)⁻¹, mul_inf, mul_one, mul_left_inv, mul_comm, ← div_eq_mul_inv,
  pos_div_neg, neg_eq_inv_inf_one, inv_inv]