proposition: Lemma quot_add : forall a b c, c~=0 -> 0 <= (a+b*c)*a -> (a + b * c) ÷ c == a ÷ c + b.
proof: Proof. intros a b c **. rewrite <- (mul_cancel_l _ _ c) by trivial. rewrite <- (add_cancel_r _ _ ((a+b*c) rem c)). rewrite <- quot_rem, rem_add by trivial. now rewrite mul_add_distr_l, add_shuffle0, <-quot_rem, mul_comm. Qed.
imports: ZAxioms ZMulOrder ZSgnAbs NZDiv