proposition: Lemma Zdiv_same : forall a : Z, a <> 0%Z -> (a / a)%Z = 1%Z.
proof: Proof. intros a. case a. tauto. intros; apply Z_div_same; auto with zarith. intros A HA. fold (- Zpos A)%Z in |- *. rewrite Zdiv_Zopp. simpl in |- *. replace (Zpos A) with (Z.abs (Zneg A)); auto. rewrite Zabs_div_rht. auto. replace (- Zpos A)%Z with (-1 * Zpos A)%Z; auto with zarith. apply Zmod_mult_cancel_rht. Qed.
imports: CoRN.model.Zmod.ZBasics