proposition: Lemma inverse_inverse : forall a u, invertible a u -> inverse a (inverse a u) = u.
proof: Proof. ir. apply inverse_unique with a (inverse a u). ap invertible_inverse. ap inverse_invertible. am. ap are_inverse_symm. ap invertible_inverse. am. Qed.
imports: Arith universe