proposition: Lemma ring_S_inj x y : 1+x==1+y -> x==y.
proof: Proof. intros. rewrite <- (ARadd_0_l ARth x), <- (ARadd_0_l ARth y). rewrite <- (Ropp_def Rth 1), (ARadd_comm ARth 1). rewrite <- !(ARadd_assoc ARth). now apply (Radd_ext Reqe). Qed.
imports: ZArith_base