proposition: Theorem interval_eq : forall p q q', p*q'-p < p*q <= p*q' -> q=q'.
proof: Proof. intros p; case p. - simpl; intros q q' (Hlt, Hle); elim (Nat.lt_irrefl 0);assumption. - intros p' q q' (Hlt, Hle). apply Nat.le_antisymm. + apply (Nat.mul_le_mono_pos_l _ _ (S p')); [apply Nat.lt_0_succ|auto]. + assert (Hlt' : (q' - 1)*S p' < S p' * q). { rewrite Nat.mul_sub_distr_r. rewrite Nat.mul_1_l. rewrite (Nat.mul_comm q'). assumption. } rewrite (Nat.mul_comm (q' - 1)) in Hlt'. generalize (mult_lt_reg_l _ _ _ Hlt'). case q'; simpl. * auto with arith. * intros n; rewrite Nat.sub_0_r; auto with arith. Qed.
imports: List Arith