proposition: Lemma Ropp_opp x : - -x == x.
proof: Proof. rewrite <- (Radd_0_l Rth (- -x)). rewrite <- (Ropp_def Rth x). rewrite <- (Radd_assoc Rth), (Ropp_def Rth). rewrite ((Radd_comm Rth) x); now apply (Radd_0_l Rth). Qed.
imports: Setoid Morphisms BinPos BinNat