proposition: Lemma modulo : forall n, n > 0 -> forall m:nat, {r : nat | exists q : nat, m = q * n + r /\ n > r}.
proof: Proof. intros n H m; induction m as (m,H0) using gt_wf_rec. destruct (le_gt_dec n m) as [Hlebn|Hgtbn]. - destruct (H0 (m - n)) as (r & Hr); [ apply Nat.sub_lt; auto | ]. exists r; destruct Hr as (q & Heq & Hgt); exists (S q); split; trivial. simpl; rewrite <- Nat.add_assoc, <- Heq, Nat.add_comm, Nat.sub_add; trivial. - exists m; exists 0; simpl; auto. Defined.
imports: PeanoNat Compare_dec Wf_nat