proposition: Lemma Euc1 : forall b q q' r r', 0 < b -> q*b + r = q'*b + r' -> r < b -> r' < b -> q = q'.
proof: Proof. intros; case (lt_eq_lt_dec q q'). destruct 1. assert (S q <= q'). auto with arith. assert ((S q)*b + r <= q' *b + r). apply plus_le_compat_r. apply mult_le_compat_r. auto. simpl in H4. rewrite <- plus_assoc in H4. rewrite H0 in H4. omega. auto. intro. assert (S q' <= q). auto with arith. assert ((S q')*b + r <= q *b + r). apply plus_le_compat_r. apply mult_le_compat_r. auto. simpl in H4. rewrite <- plus_assoc in H4. rewrite H0 in H4. omega. Qed.
imports: Arith ArithRing Compare_dec Omega Max