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