x : -x = x * -1. Proof. apply (right_cancellation (+) x). transitivity (x * -1 + x * 1). - lhs apply left_inverse. rhs_V rapply simple_distribute_l. lhs_V rapply (right_absorb x). apply (ap (x *.)). symmetry. apply left_inverse. - f_ap. apply right_identity. Defined.
Require Import Require Import