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