Semigroup/Group proof

Definition associativity (T : Set) (o : T -> T -> T) :=
  forall x y z, (o (o x y) z) = (o x (o y z)).

Record Semigroup : Type := makeSemigroup {
  T : Set;
  o : T -> T -> T;
  assoc : associativity T o
}.

Record Group : Type := makeGroup {
  T' : Set;
  o' : T' -> T' -> T';
  assoc' : associativity T' o';
  I : T';
  unit' : forall u : T', exists v, o' u v = I
}.

(* Any semigroup S with a right unit, and right inverse forall a in
   S is a group *)

Theorem ex10
  (S : Semigroup)
  (right_unit : T S)
  (right_unit_meaning : forall a, (o S) a right_unit = a)
  (right_inverse : forall a, exists b, (o S) a b = right_unit)
: (* --------------------------------------------------------- *)
  exists I : T S,
    forall u : T S, exists v, (o S) u v = I.

intros.
exists right_unit.

intro.

destruct (right_inverse u).
exists x.

assumption.
Qed.