proposition: Lemma chRem2 : forall b1 r1 b2 r2 q : Z, (0 <= r1)%Z -> (0 <= r2)%Z -> (r1 < q)%Z -> (r2 < q)%Z -> (b1 * q + r1)%Z = (b2 * q + r2)%Z -> r1 = r2.
proof: Proof. intros * H H0 H1 H2 H3. assert (H4: ((b1 - b2) * q)%Z = (r2 - r1)%Z) by (rewrite Z.mul_sub_distr_r; lia). induction (Zle_or_lt 0 (b1 - b2)) as [H5 | H5]. induction (Zle_lt_or_eq _ _ H5) as [H6 | H6]. assert (H7: (1 <= b1 - b2)%Z). { replace 1%Z with (Z.succ 0) by reflexivity. now apply Zlt_le_succ. } assert (H8: (q <= r2 - r1)%Z). { replace q with (1 * q)%Z by apply Zmult_1_l. - rewrite <- H4. apply Zmult_le_compat_r. + assumption. + eapply Z.le_trans. * apply H. * now apply Zlt_le_weak. } set (A1 := Zplus_lt_le_compat r2 q (- r1) 0 H2) in *. assert (H9: (r2 - r1 < q)%Z). { replace q with (q + 0)%Z by ( now rewrite <- Zplus_0_r_reverse). unfold Zminus in |- *; apply A1. eapply (fun a b : Z => Zplus_le_reg_l a b r1). rewrite Zplus_opp_r. now rewrite <- Zplus_0_r_reverse. } destruct (Zle_not_lt q (r2 - r1)). assumption. assumption. rewrite <- H6, Z.mul_comm in H4. rewrite <- Zmult_0_r_reverse in H4. rewrite <- (Zplus_opp_r r2) in H4. unfold Zminus in H4. apply Z.opp_inj. symmetry in |- *; eapply Zplus_reg_l. apply H4. assert (H6: (1 <= b2 - b1)%Z). { replace 1%Z with (Z.succ 0) by reflexivity. apply Zlt_le_succ. apply (Zplus_lt_reg_l 0 (b2 - b1) b1). rewrite Zplus_minus. rewrite <- Zplus_0_r_reverse. apply (Zplus_lt_reg_l b1 b2 (- b2)). rewrite Zplus_opp_l. rewrite Zplus_comm. now unfold Zminus in H5. } assert (H7: ((b2 - b1) * q)%Z = (r1 - r2)%Z) by ( rewrite Z.mul_sub_distr_r ; lia ). assert (H8:(q <= r1 - r2)%Z). { replace q with (1 * q)%Z. rewrite <- H7. apply Zmult_le_compat_r. assumption. eapply Z.le_trans. apply H. apply Zlt_le_weak. assumption. apply Zmult_1_l. } set (A1 := Zplus_lt_le_compat r1 q (- r2) 0 H1) in *. assert (H9:(r1 - r2 < q)%Z). { replace q with (q + 0)%Z. unfold Zminus in |- *. apply A1. eapply (fun a b : Z => Zplus_le_reg_l a b r2). rewrite Zplus_opp_r. now rewrite <- Zplus_0_r_reverse. now rewrite <- Zplus_0_r_reverse. } destruct (Zle_not_lt q (r1 - r2)); assumption. Qed.
imports: Arith Wf_nat ZArith Peano_dec ZArith_dec NatAux ZCAux ZCmisc ZSum Pmod Ppow