Idris Group Problem

grp.idr

interface Group a where
  (<*>) : a -> a -> a
  inv : a -> a
  e : a
  lAssoc : (x <*> y) <*> z = x <*> (y <*> z)
  rAssoc : x <*> (y <*> z) = (x <*> y) <*> z
  lId : e <*> x = x
  rId : x <*> e = x
  lInv : inv x <*> x = e
  rInv : x <*> inv x = e

lMultIntro : (Group a) => {x,y : a} -> (pf : x = y) -> (z : a) -> (z <*> x = z <*> y)
lMultIntro Refl _ = Refl

rMultIntro : (Group a) => {x,y : a} -> (pf : x = y) -> (z : a) -> (x <*> z = y <*> z)
rMultIntro Refl _ = Refl

lMultElim : (Group a) =>  {x,y,z : a} -> (pf : z <*> x = z <*> y) -> (x = y)
lMultElim {x = x} {y = y} {z = z} {pf = pf} =
  let lMult = lMultIntro pf (inv z) in
      let reassocd = trans lAssoc (trans lMult rAssoc) in
          let xElimd = trans (rMultIntro lInv x) lId in
          let yElimd = trans (rMultIntro lInv y) lId in
              trans (sym xElimd) (trans reassocd yElimd)

rMultElim : (Group a) =>  {x,y,z : a} -> (pf : x <*> z = y <*> z) -> (x = y)
rMultElim {x = x} {y = y} {z = z} {pf = pf} =
  let rMult = rMultIntro pf (inv z) in
      let reassocd = trans rAssoc (trans rMult lAssoc) in
          let xElimd = trans (lMultIntro rInv x) rId in
          let yElimd = trans (lMultIntro rInv y) rId in
              trans (sym xElimd) (trans reassocd yElimd)


invIsInvolution : (Group a) => {x : a} -> (inv (inv x)) = x
invIsInvolution = lMultElim (trans rInv (sym lInv))

lDivOut : (Group a) => {x,y,z : a} -> (x <*> y = z) -> (y = (inv x) <*> z)
lDivOut Refl {x = x} {y = y} = sym $ trans rAssoc (trans (rMultIntro lInv y) lId)

rDivOut : (Group a) => {x,y,z : a} -> (x <*> y = z) -> (x = z <*> (inv y))
rDivOut Refl {x = x} {y = y} = sym $ trans lAssoc (trans (lMultIntro rInv x) rId)

prodInv : (Group a) => {x,y : a} -> (inv (x <*> y) = (inv y) <*> (inv x))
prodInv {x = x} {y = y} = let yInv : (e = (inv y) <*> y) = (sym lInv) in
                              let comb = trans (lInv {x=x}) yInv in
                                  ?h