proposition: Lemma sgn_sgn : forall x, sgn (sgn x) == sgn x.
proof: Proof. intros x. destruct (sgn_spec x) as [(LT,EQ)|[(EQ',EQ)|(LT,EQ)]]; rewrite EQ. - apply sgn_pos, lt_0_1. - now apply sgn_null. - apply sgn_neg. rewrite opp_neg_pos. apply lt_0_1. Qed.
imports: ZMulOrder