x : -x = - 1 * x. Proof. apply (left_cancellation (+) x). path_via 0. - apply right_inverse. - path_via (1 * x + (- 1) * x). + apply symmetry. rewrite <-distribute_r. rewrite right_inverse. apply left_absorb. + apply ap011;try reflexivity. apply left_identity. Qed.
Require Import Require Import