proposition: Theorem div_mod_unique : forall b q1 q2 r1 r2, 0<=r1<b -> 0<=r2<b -> b*q1+r1 == b*q2+r2 -> q1 == q2 /\ r1 == r2.
proof: Proof. intros b. assert (U : forall q1 q2 r1 r2, b*q1+r1 == b*q2+r2 -> 0<=r1<b -> 0<=r2 -> q1<q2 -> False). - intros q1 q2 r1 r2 EQ LT Hr1 Hr2. contradict EQ. apply lt_neq. apply lt_le_trans with (b*q1+b). + rewrite <- add_lt_mono_l. tauto. + apply le_trans with (b*q2). * rewrite mul_comm, <- mul_succ_l, mul_comm. apply mul_le_mono_nonneg_l; intuition; try order. rewrite le_succ_l; auto. * rewrite <- (add_0_r (b*q2)) at 1. rewrite <- add_le_mono_l. tauto. - intros q1 q2 r1 r2 Hr1 Hr2 EQ; destruct (lt_trichotomy q1 q2) as [LT|[EQ'|GT]]. + elim (U q1 q2 r1 r2); intuition. + split; auto. rewrite EQ' in EQ. rewrite add_cancel_l in EQ; auto. + elim (U q2 q1 r2 r1); intuition auto with relations. Qed.
imports: NZAxioms NZMulOrder