proposition: Lemma posZ_Zsgn2 : forall x : Z, x <> 0%Z -> (Z.sgn x * x)%Z = posZ x.
proof: Proof. simple induction x; intros; [ elim H | simpl in |- * | simpl in |- * ]; reflexivity. Qed.
imports: Coq.ZArith.ZArith CoRN.logic.CLogic Coq.Setoids.Setoid