proposition: Lemma mod_sign_nz : forall a b, b~=0 -> a mod b ~= 0 -> sgn (a mod b) == sgn b.
proof: Proof. intros a b Hb H. destruct (lt_ge_cases 0 b) as [Hb'|Hb']. - destruct (mod_pos_bound a b Hb'). rewrite 2 sgn_pos; order. - destruct (mod_neg_bound a b). + order. + rewrite 2 sgn_neg; order. Qed.
imports: ZAxioms ZMulOrder ZSgnAbs NZDiv