proposition: Lemma rem_sign_nz : forall a b, b~=0 -> a rem b ~= 0 -> sgn (a rem b) == sgn a.
proof: Proof. intros a b Hb H. destruct (lt_trichotomy 0 a) as [LT|[EQ|LT]]. - rewrite 2 sgn_pos; try easy. generalize (rem_nonneg a b Hb (lt_le_incl _ _ LT)). order. - now rewrite <- EQ, rem_0_l, sgn_0. - rewrite 2 sgn_neg; try easy. generalize (rem_nonpos a b Hb (lt_le_incl _ _ LT)). order. Qed.
imports: ZAxioms ZMulOrder ZSgnAbs NZDiv