proposition: Lemma Zabs_div_rht : forall a : Z, (a / Z.abs a)%Z = Z.sgn a.
proof: Proof. intro a. set (A := Z.abs a). set (sa := Z.sgn a). replace a with (Z.abs a * Z.sgn a)%Z. unfold sa in |- *; clear sa. case (Zdec A). unfold A in |- *; intro HA. cut (a = 0%Z); auto with zarith. intro Ha; rewrite Ha; auto with zarith. unfold A in |- *; apply Zdiv_mult_cancel_lft. rewrite Zmult_comm. auto with zarith. Qed.
imports: CoRN.model.Zmod.ZBasics