proposition: Lemma mod_sign : forall a b, b~=0 -> sgn (a mod b) ~= -sgn b.
proof: Proof. intros a b Hb H. destruct (eq_decidable (a mod b) 0) as [EQ|NEQ]. - apply Hb, sgn_null_iff, opp_inj. now rewrite <- H, opp_0, EQ, sgn_0. - apply Hb, sgn_null_iff. apply eq_mul_0_l with 2; try order'. nzsimpl'. apply add_move_0_l. rewrite <- H. symmetry. now apply mod_sign_nz. Qed.
imports: ZAxioms ZMulOrder ZSgnAbs NZDiv