proposition: Lemma chRem1 : forall b : nat, b > 0 -> forall a : Z, {p : Z * nat | snd p < b /\ Z.of_nat (snd p) = (fst p * Z.of_nat b + a)%Z}.
proof: Proof. intros b H a. assert (H0: forall a' : Z, (a' >= 0)%Z -> {p : Z * nat | snd p < b /\ Z.of_nat (snd p) = (fst p * Z.of_nat b + a')%Z}). { intros a' H0; set (A := Z.to_nat a') in *. induction (div_eucl b H A) as [x p]. destruct x as (a0, b0). exists ((- Z.of_nat a0)%Z, b0). destruct p as (H1, H2). split. - apply H2. - rewrite <- (Z2Nat.id a'). + simpl fst ; simpl snd. rewrite Zopp_mult_distr_l_reverse. rewrite Z.add_comm. fold (Z.of_nat (Z.to_nat a') - Z.of_nat a0 * Z.of_nat b)%Z in |- *. apply Zplus_minus_eq. rewrite <- Znat.inj_mult. rewrite <- Znat.inj_plus. apply Znat.inj_eq. apply H1. + auto. now rewrite <- Z.ge_le_iff. } destruct (Z_ge_lt_dec a 0) as [g | l]. + apply H0; assumption. + assert (a + Z.of_nat b * - a >= 0)%Z. induction b as [| b Hrecb]. * elim (Nat.lt_irrefl _ H). * rewrite Znat.inj_S. rewrite Z.mul_comm. rewrite <- Zmult_succ_r_reverse. fold (- a * Z.of_nat b - a)%Z in |- *. rewrite Zplus_minus. replace 0%Z with (0 * Z.of_nat b)%Z. apply Zmult_ge_compat_r. rewrite (Zminus_diag_reverse a). rewrite <- (Zplus_0_l (- a)). unfold Zminus in |- *; apply Z.le_ge. apply Zplus_le_compat_r. now apply Zlt_le_weak. change 0%Z with (Z.of_nat 0). apply Znat.inj_ge. unfold ge in |- *. apply Nat.le_0_l. auto. * destruct (H0 _ H1) as [(a0,b1) [H2 H3]]. exists ((a0 - a)%Z, b1); split. -- simpl in |- *; apply H2. -- cbv beta iota zeta delta [fst snd] in H3 |- *. rewrite H3, (Zplus_comm a), Zplus_assoc. apply Zplus_eq_compat. rewrite Zmult_minus_distr_r. unfold Zminus in |- *. apply Zplus_eq_compat. reflexivity. rewrite Z.mul_comm. apply Zopp_mult_distr_l_reverse. reflexivity. Qed.
imports: Arith Wf_nat ZArith Peano_dec ZArith_dec NatAux ZCAux ZCmisc ZSum Pmod Ppow