proposition: Lemma divmod_spec : forall x y q u, u <= y -> let (q',u') := divmod x y q u in x + (S y)*q + (y-u) = (S y)*q' + (y-u') /\ u' <= y.
proof: Proof. intro x; induction x as [|x IHx]. - simpl; intuition. - intros y q u H. destruct u as [|u]; simpl divmod. + generalize (IHx y (S q) y (le_n y)). destruct divmod as (q',u'). intros (EQ,LE); split; trivial. rewrite <- EQ, sub_0_r, sub_diag, add_0_r. now rewrite !add_succ_l, <- add_succ_r, <- add_assoc, mul_succ_r. + assert (H' : u <= y). { apply le_trans with (S u); trivial. do 2 constructor. } generalize (IHx y q u H'). destruct divmod as (q',u'). intros (EQ,LE); split; trivial. rewrite <- EQ, !add_succ_l, <- add_succ_r; f_equal. now rewrite <- sub_succ_l. Qed.
imports: NAxioms NProperties OrdersFacts DecidableClass