/- Define a "nonzero" type -/
import algebra.group
universe u
variables {M : Type*}
structure nonzero (α : Type u) [C : has_zero α] :=
(val : α)
(not_zero : val ≠ 0)
namespace nonzero
variable [has_zero M]
instance : has_coe (nonzero M) M := ⟨val⟩
@[ext] theorem ext : function.injective (coe : nonzero M → M)
| ⟨v, h₁⟩ ⟨v', h₂⟩ e := by change v = v' at e; subst v'
@[simp] theorem mk_coe (u : nonzero M) (h₁) : mk (u : M) h₁ = u := ext rfl
@[simp] lemma val_eq_coe (a : nonzero M) : a.val = (↑a : M) := rfl
end nonzero

/-- The meat starts here -/

@[reducible, simp] --a new structure where we forcibly add "0"
def with0 (T : Type*) := option T

@[reducible, simp] --a new has_mul where we forcibly remove "0"
def drop0 (T : Type*) [has_zero T] := nonzero T

instance : has_zero (with0 M) := { zero := none }

open classical
local attribute [instance] prop_decidable

noncomputable def iso [sl : has_zero M]: with0 (drop0 M) ≃ M :=
{
to_fun := λ a, option.rec_on a 0 nonzero.val,
inv_fun := λ a, dite (a=0) (λ _, none) (λ h, option.some (nonzero.mk a h)),
left_inv := begin
    intro a, cases a; simp, cases a, contradiction,
  end,
right_inv := begin
    intro a, by_cases a=0,
      {
        simp [h],
        sorry
      },{
        simp [h],
        sorry,
      }
  end
}