proposition: Lemma eucl_dev : forall n, n > 0 -> forall m:nat, diveucl m n.
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 (q,r,Hge0,Heq); [ apply Nat.sub_lt; auto | ]. apply divex with (S q) r; trivial. simpl; rewrite <- Nat.add_assoc, <- Heq, Nat.add_comm, Nat.sub_add; trivial. - apply divex with 0 m; simpl; trivial. Defined.
imports: PeanoNat Compare_dec Wf_nat