proposition: Lemma div_eucl : forall b : nat, b > 0 -> forall a : nat, {p : nat * nat | a = fst p * b + snd p /\ b > snd p}.
proof: Proof. intros b H a; apply (gt_wf_rec a). intros n H0 . destruct (le_lt_dec b n) as [Hle | Hlt]. - assert (n > n - b). { unfold gt in |- *; apply Nat.sub_lt; assumption. } destruct (H0 _ H1) as [[a1 b0] p]. simpl in p; exists (S a1, b0); simpl in |- *. destruct p as (H2, H3). split; [| assumption]. + rewrite <- Nat.add_assoc, <- H2. now rewrite Nat.add_comm, Nat.sub_add. - exists (0, n); simpl in |- *; now split. Qed.
imports: Arith Wf_nat ZArith Peano_dec ZArith_dec NatAux ZCAux ZCmisc ZSum Pmod Ppow