proposition: Lemma div_0_l: forall a, a~=0 -> 0/a == 0.
proof: Proof. intros. pos_or_neg a. - apply div_0_l; order. - apply opp_inj. rewrite <- div_opp_r, opp_0 by trivial. now apply div_0_l. Qed.
imports: ZAxioms ZMulOrder ZSgnAbs NZDiv