https://twitter.com/bd_gfngfn/status/716086088549294080

group_description.v

Require Import Coq.Logic.Description.

Parameter G : Type.
Parameter mult : G -> G -> G.
Axiom ax :
  (forall x y z, mult x (mult y z) = mult (mult x y) z) /\
  (exists e, forall x,
    mult e x = x /\ x = mult x e /\
    exists i, mult x i = e /\ e = mult i x).

Definition assoc := proj1 ax.
Lemma e_construction : { e | forall x,
    mult e x = x /\ x = mult x e /\
    exists i, mult x i = e /\ e = mult i x }.
Proof.
  apply constructive_definite_description.
  destruct (proj2 ax) as [e He].
  exists e; split; [exact He|].
  intros e' He'.
  transitivity (mult e e').
  - apply He'.
  - apply He.
Qed.
Definition e := proj1_sig e_construction.
Definition el x : mult e x = x := proj1 (proj2_sig e_construction x).
Definition er x : mult x e = x :=
  eq_sym (proj1 (proj2 (proj2_sig e_construction x))).
Definition inverse_ax x : exists i, mult x i = e /\ e = mult i x
  := proj2 (proj2 (proj2_sig e_construction x)).
Lemma i_construction x : { i | mult x i = e /\ e = mult i x }.
Proof.
  apply constructive_definite_description.
  destruct (inverse_ax x) as [i Hi].
  exists i; split; [exact Hi|].
  intros i' Hi'.
  rewrite <-(er i).
  rewrite <-(proj1 Hi').
  rewrite assoc.
  rewrite <-(proj2 Hi).
  rewrite el.
  reflexivity.
Qed.
Definition inv x := proj1_sig (i_construction x).
Definition inv_l x : mult (inv x) x = e :=
  eq_sym (proj2 (proj2_sig (i_construction x))).
Definition inv_r x : mult x (inv x) = e :=
  proj1 (proj2_sig (i_construction x)).