proposition: Theorem Zdiv_sgn: forall a b, 0 <= Z.sgn (a/b) * Z.sgn a * Z.sgn b.
proof: Proof. intros a b; destruct a as [ |a|a]; destruct b as [ |b|b]; simpl; auto with zarith; generalize (Z.div_pos (Zpos a) (Zpos b)); unfold Z.div, Z.div_eucl; destruct Z.pos_div_eucl as (q,r); destruct r; rewrite ?Z.mul_1_r, <-?Z.opp_eq_mul_m1, ?Z.sgn_opp, ?Z.opp_involutive; match goal with [|- (_ -> _ -> ?P) -> _] => intros HH; assert (HH1 : P); auto with zarith end; apply Z.sgn_nonneg; auto with zarith. Qed.
imports: ZArith_base Zbool ZArithRing Zcomplements Setoid Morphisms