proposition: Lemma quot_div_exact : forall a b, b~=0 -> (b|a) -> a÷b == a/b.
proof: Proof. intros a b Hb H. apply mul_cancel_l with b; trivial. assert (H':=H). apply rem_divide, quot_exact in H; trivial. apply mod_divide, div_exact in H'; trivial. now rewrite <-H,<-H'. Qed.
imports: ZAxioms ZMulOrder ZSgnAbs ZGcd ZDivTrunc ZDivFloor