proposition: Lemma Zdiv_Zopp : forall a b : Z, (a mod b)%Z = 0%Z -> (a / - b)%Z = (- (a / b))%Z.
proof: Proof. intros a b. unfold Z.modulo, Z.div, Z.div_eucl in |- *. case a. auto. intro A. case b; unfold Z.opp in |- *. auto. intro B. elim (Coq.ZArith.BinIntDef.Z.pos_div_eucl A (Zpos B)); intros q r. intro Hr; rewrite Hr; auto. intro B. generalize (Z_mod_lt (Zpos A) (Zpos B)). unfold Z.modulo, Z.div_eucl in |- *. elim (Coq.ZArith.BinIntDef.Z.pos_div_eucl A (Zpos B)); intros q r. case r. intros _ HR; fold (- q)%Z in |- *; fold (- - q)%Z in |- *; rewrite Z.opp_involutive; auto. intros R Hlt HR. assert (H : Zpos R = Zpos B). rewrite <- (Zplus_0_r (Zpos B)); rewrite <- HR; rewrite Zplus_assoc; fold (- Zpos B)%Z in |- *. auto with zarith. rewrite H in Hlt. elim Hlt; auto with zarith. intros R Hlt HR. elim Hlt; auto with zarith; intro Hfalse; elim Hfalse; auto with zarith. intro A. case b; unfold Z.opp in |- *. auto. intro B. generalize (Z_mod_lt (Zpos A) (Zpos B)). unfold Z.modulo, Z.div_eucl in |- *. elim (Coq.ZArith.BinIntDef.Z.pos_div_eucl A (Zpos B)); intros q r. case r. intros _ HR; fold (- q)%Z in |- *; fold (- - q)%Z in |- *; rewrite Z.opp_involutive; auto. intros R Hlt HR. assert (H : Zpos R = Zpos B). rewrite <- (Zplus_0_r (Zpos R)); rewrite <- HR; unfold Zminus in |- *; rewrite Zplus_assoc; auto with zarith. rewrite H in Hlt. elim Hlt; auto with zarith. intros R Hlt HR. elim Hlt; auto with zarith; intro Hfalse; elim Hfalse; auto with zarith. intro B. generalize (Z_mod_lt (Zpos A) (Zpos B)). unfold Z.modulo, Z.div_eucl in |- *. elim (Coq.ZArith.BinIntDef.Z.pos_div_eucl A (Zpos B)); intros q r. case r. intros _ HR; fold (- q)%Z in |- *; auto. intros; discriminate. intros; discriminate. Qed.
imports: CoRN.model.Zmod.ZBasics