proposition: Lemma Zdivisor_small : forall a b : Z, Zdivides b a -> (Z.abs a < b)%Z -> a = 0%Z.
proof: Proof. intros a b Hdiv Hlt. generalize (Zdivides_abs_elim_rht _ _ Hdiv); intro Hdivabs. set (A := a). assert (HA : A = a). auto. generalize HA. case A. auto. intros p Hp. assert (Hfalse : (b < b)%Z). apply (Z.le_lt_trans b (Z.abs a) b). apply Z.ge_le. apply (Zdivisor_pos_le (Z.abs a) b). rewrite <- Hp; simpl in |- *; auto with zarith. assumption. assumption. elim (Z.lt_irrefl b Hfalse). intros p Hp. assert (Hfalse : (b < b)%Z). apply (Z.le_lt_trans b (Z.abs a) b). apply Z.ge_le. apply (Zdivisor_pos_le (Z.abs a) b). rewrite <- Hp; simpl in |- *. auto with zarith. assumption. assumption. elim (Z.lt_irrefl b Hfalse). Qed.
imports: CoRN.model.Zmod.ZBasics