proposition: Lemma unique_identity e': (forall z, op e' z = z) -> e' = e.
proof: Proof. Proof using associative identity inverse HG. intros pe'. verit (associative, identity, inverse, pe'). Qed.
imports: SMTCoq Bool PArray Int63 List ZArith