From 832af2271f05b0d238145733abc422588a07ee3c Mon Sep 17 00:00:00 2001 From: William Ball Date: Fri, 6 Dec 2024 16:30:44 -0800 Subject: [PATCH] right inverse unique --- examples/algebra.pg | 30 ++++++++++++++++++++++++++++++ 1 file changed, 30 insertions(+) diff --git a/examples/algebra.pg b/examples/algebra.pg index d178b49..1f00907 100644 --- a/examples/algebra.pg +++ b/examples/algebra.pg @@ -161,4 +161,34 @@ section Group -- e * a^-1 = a^-1 (id_lg (i a))))); + -- And so are right inverses + def right_inv_unique (a b : G) (h : right_inverse a b) : eq G b (i a) := + -- b = e * b + -- = (a^-1 * a) * b + -- = a^-1 * (a * b) + -- = a^-1 * e + -- = a^-1 + eq_trans G b (op e b) (i a) + -- b = e * b + (eq_sym G (op e b) b (id_lg b)) + -- e * b = a^-1 + (eq_trans G (op e b) (op (op (i a) a) b) (i a) + -- e * b = (a^-1 * a) * b + (eq_cong G G e (op (i a) a) (fun (x : G) => op x b) + -- e = (a^-1 * a) + (eq_sym G (op (i a) a) e (inv_lg a))) + + -- (a^-1 * a) * b = a^-1 + (eq_trans G (op (op (i a) a) b) (op (i a) (op a b)) (i a) + -- (a^-1 * a) * b = a^-1 * (a * b) + (eq_sym G (op (i a) (op a b)) (op (op (i a) a) b) (assoc_g (i a) a b)) + + -- a^-1 * (a * b) = a^-1 + (eq_trans G (op (i a) (op a b)) (op (i a) e) (i a) + -- a^-1 * (a * b) = a^-1 * e + (eq_cong G G (op a b) e (op (i a)) h) + + -- a^-1 * e = a^-1 + (id_rg (i a))))); + end Group